<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><link rel="stylesheet" type="text/css" href="style.css" /><script type="text/javascript" src="highlight.js"></script></head><body><pre><span id="local-6989586621680837460"><span id="local-6989586621680837461"><span id="local-6989586621680837462"><span id="local-6989586621680837463"><span id="local-6989586621680837464"></span></span></span></span></span><span class="hs-pragma">{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveFoldable,
             DeriveTraversable #-}</span><span>
</span><span id="line-3"></span><span>
</span><span id="line-4"></span><span class="hs-comment">--------------------------------------------------------------------------------</span><span>
</span><span id="line-5"></span><span class="hs-comment">-- | Boolean formulas without quantifiers and without negation.</span><span>
</span><span id="line-6"></span><span class="hs-comment">-- Such a formula consists of variables, conjunctions (and), and disjunctions (or).</span><span>
</span><span id="line-7"></span><span class="hs-comment">--</span><span>
</span><span id="line-8"></span><span class="hs-comment">-- This module is used to represent minimal complete definitions for classes.</span><span>
</span><span id="line-9"></span><span class="hs-comment">--</span><span>
</span><span id="line-10"></span><span class="hs-keyword">module</span><span> </span><span class="hs-identifier">GHC.Data.BooleanFormula</span><span> </span><span class="hs-special">(</span><span>
</span><span id="line-11"></span><span>        </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier">BooleanFormula</span></a></span><span class="hs-special">(</span><span class="hs-glyph">..</span><span class="hs-special">)</span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#LBooleanFormula"><span class="hs-identifier">LBooleanFormula</span></a></span><span class="hs-special">,</span><span>
</span><span id="line-12"></span><span>        </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#mkFalse"><span class="hs-identifier">mkFalse</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#mkTrue"><span class="hs-identifier">mkTrue</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#mkAnd"><span class="hs-identifier">mkAnd</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#mkOr"><span class="hs-identifier">mkOr</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#mkVar"><span class="hs-identifier">mkVar</span></a></span><span class="hs-special">,</span><span>
</span><span id="line-13"></span><span>        </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#isFalse"><span class="hs-identifier">isFalse</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#isTrue"><span class="hs-identifier">isTrue</span></a></span><span class="hs-special">,</span><span>
</span><span id="line-14"></span><span>        </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#eval"><span class="hs-identifier">eval</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#simplify"><span class="hs-identifier">simplify</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#isUnsatisfied"><span class="hs-identifier">isUnsatisfied</span></a></span><span class="hs-special">,</span><span>
</span><span id="line-15"></span><span>        </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#implies"><span class="hs-identifier">implies</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#impliesAtom"><span class="hs-identifier">impliesAtom</span></a></span><span class="hs-special">,</span><span>
</span><span id="line-16"></span><span>        </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#pprBooleanFormula"><span class="hs-identifier">pprBooleanFormula</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#pprBooleanFormulaNice"><span class="hs-identifier">pprBooleanFormulaNice</span></a></span><span>
</span><span id="line-17"></span><span>  </span><span class="hs-special">)</span><span> </span><span class="hs-keyword">where</span><span>
</span><span id="line-18"></span><span>
</span><span id="line-19"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="GHC.Prelude.html"><span class="hs-identifier">GHC.Prelude</span></a></span><span>
</span><span id="line-20"></span><span>
</span><span id="line-21"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="../../base/src/Data.List.html#"><span class="hs-identifier">Data.List</span></a></span><span> </span><span class="hs-special">(</span><span> </span><span class="annot"><a href="../../base/src/Data.OldList.html#nub"><span class="hs-identifier">nub</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="../../base/src/Data.OldList.html#intersperse"><span class="hs-identifier">intersperse</span></a></span><span> </span><span class="hs-special">)</span><span>
</span><span id="line-22"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="../../base/src/Data.Data.html#"><span class="hs-identifier">Data.Data</span></a></span><span>
</span><span id="line-23"></span><span>
</span><span id="line-24"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="GHC.Utils.Monad.html"><span class="hs-identifier">GHC.Utils.Monad</span></a></span><span>
</span><span id="line-25"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="GHC.Utils.Outputable.html"><span class="hs-identifier">GHC.Utils.Outputable</span></a></span><span>
</span><span id="line-26"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="GHC.Utils.Binary.html"><span class="hs-identifier">GHC.Utils.Binary</span></a></span><span>
</span><span id="line-27"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="GHC.Types.SrcLoc.html"><span class="hs-identifier">GHC.Types.SrcLoc</span></a></span><span>
</span><span id="line-28"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="GHC.Types.Unique.html"><span class="hs-identifier">GHC.Types.Unique</span></a></span><span>
</span><span id="line-29"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="GHC.Types.Unique.Set.html"><span class="hs-identifier">GHC.Types.Unique.Set</span></a></span><span>
</span><span id="line-30"></span><span>
</span><span id="line-31"></span><span class="hs-comment">----------------------------------------------------------------------</span><span>
</span><span id="line-32"></span><span class="hs-comment">-- Boolean formula type and smart constructors</span><span>
</span><span id="line-33"></span><span class="hs-comment">----------------------------------------------------------------------</span><span>
</span><span id="line-34"></span><span>
</span><span id="line-35"></span><span class="hs-keyword">type</span><span> </span><span id="LBooleanFormula"><span class="annot"><a href="GHC.Data.BooleanFormula.html#LBooleanFormula"><span class="hs-identifier hs-var">LBooleanFormula</span></a></span></span><span> </span><span id="local-6989586621680837443"><span class="annot"><a href="#local-6989586621680837443"><span class="hs-identifier hs-type">a</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><a href="GHC.Types.SrcLoc.html#Located"><span class="hs-identifier hs-type">Located</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837443"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-36"></span><span>
</span><span id="line-37"></span><span class="hs-keyword">data</span><span> </span><span id="BooleanFormula"><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-var">BooleanFormula</span></a></span></span><span> </span><span id="local-6989586621680837706"><span class="annot"><a href="#local-6989586621680837706"><span class="hs-identifier hs-type">a</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span id="Var"><span class="annot"><a href="GHC.Data.BooleanFormula.html#Var"><span class="hs-identifier hs-var">Var</span></a></span></span><span> </span><span class="annot"><a href="#local-6989586621680837706"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">|</span><span> </span><span id="And"><span class="annot"><a href="GHC.Data.BooleanFormula.html#And"><span class="hs-identifier hs-var">And</span></a></span></span><span> </span><span class="hs-special">[</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#LBooleanFormula"><span class="hs-identifier hs-type">LBooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837706"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">]</span><span> </span><span class="hs-glyph">|</span><span> </span><span id="Or"><span class="annot"><a href="GHC.Data.BooleanFormula.html#Or"><span class="hs-identifier hs-var">Or</span></a></span></span><span> </span><span class="hs-special">[</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#LBooleanFormula"><span class="hs-identifier hs-type">LBooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837706"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">]</span><span>
</span><span id="line-38"></span><span>                      </span><span class="hs-glyph">|</span><span> </span><span id="Parens"><span class="annot"><a href="GHC.Data.BooleanFormula.html#Parens"><span class="hs-identifier hs-var">Parens</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#LBooleanFormula"><span class="hs-identifier hs-type">LBooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837706"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-39"></span><span>  </span><span class="hs-keyword">deriving</span><span> </span><span class="hs-special">(</span><span id="local-6989586621680837429"><span id="local-6989586621680837437"><span class="annot"><span class="annottext">BooleanFormula a -&gt; BooleanFormula a -&gt; Bool
(BooleanFormula a -&gt; BooleanFormula a -&gt; Bool)
-&gt; (BooleanFormula a -&gt; BooleanFormula a -&gt; Bool)
-&gt; Eq (BooleanFormula a)
forall a. Eq a =&gt; BooleanFormula a -&gt; BooleanFormula a -&gt; Bool
forall a. (a -&gt; a -&gt; Bool) -&gt; (a -&gt; a -&gt; Bool) -&gt; Eq a
/= :: BooleanFormula a -&gt; BooleanFormula a -&gt; Bool
$c/= :: forall a. Eq a =&gt; BooleanFormula a -&gt; BooleanFormula a -&gt; Bool
== :: BooleanFormula a -&gt; BooleanFormula a -&gt; Bool
$c== :: forall a. Eq a =&gt; BooleanFormula a -&gt; BooleanFormula a -&gt; Bool
</span><span class="hs-identifier hs-var hs-var hs-var hs-var hs-var hs-var">Eq</span></span></span></span><span class="hs-special">,</span><span> </span><span id="local-6989586621680837378"><span id="local-6989586621680837380"><span id="local-6989586621680837382"><span id="local-6989586621680837384"><span id="local-6989586621680837386"><span id="local-6989586621680837388"><span id="local-6989586621680837390"><span id="local-6989586621680837392"><span id="local-6989586621680837394"><span id="local-6989586621680837400"><span id="local-6989586621680837402"><span id="local-6989586621680837404"><span id="local-6989586621680837411"><span id="local-6989586621680837419"><span class="annot"><span class="annottext">Typeable (BooleanFormula a)
Typeable (BooleanFormula a)
-&gt; (forall (c :: * -&gt; *).
    (forall d b. Data d =&gt; c (d -&gt; b) -&gt; d -&gt; c b)
    -&gt; (forall g. g -&gt; c g)
    -&gt; BooleanFormula a
    -&gt; c (BooleanFormula a))
-&gt; (forall (c :: * -&gt; *).
    (forall b r. Data b =&gt; c (b -&gt; r) -&gt; c r)
    -&gt; (forall r. r -&gt; c r) -&gt; Constr -&gt; c (BooleanFormula a))
-&gt; (BooleanFormula a -&gt; Constr)
-&gt; (BooleanFormula a -&gt; DataType)
-&gt; (forall (t :: * -&gt; *) (c :: * -&gt; *).
    Typeable t =&gt;
    (forall d. Data d =&gt; c (t d)) -&gt; Maybe (c (BooleanFormula a)))
-&gt; (forall (t :: * -&gt; * -&gt; *) (c :: * -&gt; *).
    Typeable t =&gt;
    (forall d e. (Data d, Data e) =&gt; c (t d e))
    -&gt; Maybe (c (BooleanFormula a)))
-&gt; ((forall b. Data b =&gt; b -&gt; b)
    -&gt; BooleanFormula a -&gt; BooleanFormula a)
-&gt; (forall r r'.
    (r -&gt; r' -&gt; r)
    -&gt; r -&gt; (forall d. Data d =&gt; d -&gt; r') -&gt; BooleanFormula a -&gt; r)
-&gt; (forall r r'.
    (r' -&gt; r -&gt; r)
    -&gt; r -&gt; (forall d. Data d =&gt; d -&gt; r') -&gt; BooleanFormula a -&gt; r)
-&gt; (forall u.
    (forall d. Data d =&gt; d -&gt; u) -&gt; BooleanFormula a -&gt; [u])
-&gt; (forall u.
    Int -&gt; (forall d. Data d =&gt; d -&gt; u) -&gt; BooleanFormula a -&gt; u)
-&gt; (forall (m :: * -&gt; *).
    Monad m =&gt;
    (forall d. Data d =&gt; d -&gt; m d)
    -&gt; BooleanFormula a -&gt; m (BooleanFormula a))
-&gt; (forall (m :: * -&gt; *).
    MonadPlus m =&gt;
    (forall d. Data d =&gt; d -&gt; m d)
    -&gt; BooleanFormula a -&gt; m (BooleanFormula a))
-&gt; (forall (m :: * -&gt; *).
    MonadPlus m =&gt;
    (forall d. Data d =&gt; d -&gt; m d)
    -&gt; BooleanFormula a -&gt; m (BooleanFormula a))
-&gt; Data (BooleanFormula a)
BooleanFormula a -&gt; DataType
BooleanFormula a -&gt; Constr
(forall b. Data b =&gt; b -&gt; b)
-&gt; BooleanFormula a -&gt; BooleanFormula a
forall {a}. Data a =&gt; Typeable (BooleanFormula a)
forall a. Data a =&gt; BooleanFormula a -&gt; DataType
forall a. Data a =&gt; BooleanFormula a -&gt; Constr
forall a.
Data a =&gt;
(forall b. Data b =&gt; b -&gt; b)
-&gt; BooleanFormula a -&gt; BooleanFormula a
forall a u.
Data a =&gt;
Int -&gt; (forall d. Data d =&gt; d -&gt; u) -&gt; BooleanFormula a -&gt; u
forall a u.
Data a =&gt;
(forall d. Data d =&gt; d -&gt; u) -&gt; BooleanFormula a -&gt; [u]
forall a r r'.
Data a =&gt;
(r -&gt; r' -&gt; r)
-&gt; r -&gt; (forall d. Data d =&gt; d -&gt; r') -&gt; BooleanFormula a -&gt; r
forall a r r'.
Data a =&gt;
(r' -&gt; r -&gt; r)
-&gt; r -&gt; (forall d. Data d =&gt; d -&gt; r') -&gt; BooleanFormula a -&gt; r
forall a (m :: * -&gt; *).
(Data a, Monad m) =&gt;
(forall d. Data d =&gt; d -&gt; m d)
-&gt; BooleanFormula a -&gt; m (BooleanFormula a)
forall a (m :: * -&gt; *).
(Data a, MonadPlus m) =&gt;
(forall d. Data d =&gt; d -&gt; m d)
-&gt; BooleanFormula a -&gt; m (BooleanFormula a)
forall a (c :: * -&gt; *).
Data a =&gt;
(forall b r. Data b =&gt; c (b -&gt; r) -&gt; c r)
-&gt; (forall r. r -&gt; c r) -&gt; Constr -&gt; c (BooleanFormula a)
forall a (c :: * -&gt; *).
Data a =&gt;
(forall d b. Data d =&gt; c (d -&gt; b) -&gt; d -&gt; c b)
-&gt; (forall g. g -&gt; c g) -&gt; BooleanFormula a -&gt; c (BooleanFormula a)
forall a (t :: * -&gt; *) (c :: * -&gt; *).
(Data a, Typeable t) =&gt;
(forall d. Data d =&gt; c (t d)) -&gt; Maybe (c (BooleanFormula a))
forall a (t :: * -&gt; * -&gt; *) (c :: * -&gt; *).
(Data a, Typeable t) =&gt;
(forall d e. (Data d, Data e) =&gt; c (t d e))
-&gt; Maybe (c (BooleanFormula a))
forall a.
Typeable a
-&gt; (forall (c :: * -&gt; *).
    (forall d b. Data d =&gt; c (d -&gt; b) -&gt; d -&gt; c b)
    -&gt; (forall g. g -&gt; c g) -&gt; a -&gt; c a)
-&gt; (forall (c :: * -&gt; *).
    (forall b r. Data b =&gt; c (b -&gt; r) -&gt; c r)
    -&gt; (forall r. r -&gt; c r) -&gt; Constr -&gt; c a)
-&gt; (a -&gt; Constr)
-&gt; (a -&gt; DataType)
-&gt; (forall (t :: * -&gt; *) (c :: * -&gt; *).
    Typeable t =&gt;
    (forall d. Data d =&gt; c (t d)) -&gt; Maybe (c a))
-&gt; (forall (t :: * -&gt; * -&gt; *) (c :: * -&gt; *).
    Typeable t =&gt;
    (forall d e. (Data d, Data e) =&gt; c (t d e)) -&gt; Maybe (c a))
-&gt; ((forall b. Data b =&gt; b -&gt; b) -&gt; a -&gt; a)
-&gt; (forall r r'.
    (r -&gt; r' -&gt; r) -&gt; r -&gt; (forall d. Data d =&gt; d -&gt; r') -&gt; a -&gt; r)
-&gt; (forall r r'.
    (r' -&gt; r -&gt; r) -&gt; r -&gt; (forall d. Data d =&gt; d -&gt; r') -&gt; a -&gt; r)
-&gt; (forall u. (forall d. Data d =&gt; d -&gt; u) -&gt; a -&gt; [u])
-&gt; (forall u. Int -&gt; (forall d. Data d =&gt; d -&gt; u) -&gt; a -&gt; u)
-&gt; (forall (m :: * -&gt; *).
    Monad m =&gt;
    (forall d. Data d =&gt; d -&gt; m d) -&gt; a -&gt; m a)
-&gt; (forall (m :: * -&gt; *).
    MonadPlus m =&gt;
    (forall d. Data d =&gt; d -&gt; m d) -&gt; a -&gt; m a)
-&gt; (forall (m :: * -&gt; *).
    MonadPlus m =&gt;
    (forall d. Data d =&gt; d -&gt; m d) -&gt; a -&gt; m a)
-&gt; Data a
forall u.
Int -&gt; (forall d. Data d =&gt; d -&gt; u) -&gt; BooleanFormula a -&gt; u
forall u. (forall d. Data d =&gt; d -&gt; u) -&gt; BooleanFormula a -&gt; [u]
forall r r'.
(r -&gt; r' -&gt; r)
-&gt; r -&gt; (forall d. Data d =&gt; d -&gt; r') -&gt; BooleanFormula a -&gt; r
forall r r'.
(r' -&gt; r -&gt; r)
-&gt; r -&gt; (forall d. Data d =&gt; d -&gt; r') -&gt; BooleanFormula a -&gt; r
forall (m :: * -&gt; *).
Monad m =&gt;
(forall d. Data d =&gt; d -&gt; m d)
-&gt; BooleanFormula a -&gt; m (BooleanFormula a)
forall (m :: * -&gt; *).
MonadPlus m =&gt;
(forall d. Data d =&gt; d -&gt; m d)
-&gt; BooleanFormula a -&gt; m (BooleanFormula a)
forall (c :: * -&gt; *).
(forall b r. Data b =&gt; c (b -&gt; r) -&gt; c r)
-&gt; (forall r. r -&gt; c r) -&gt; Constr -&gt; c (BooleanFormula a)
forall (c :: * -&gt; *).
(forall d b. Data d =&gt; c (d -&gt; b) -&gt; d -&gt; c b)
-&gt; (forall g. g -&gt; c g) -&gt; BooleanFormula a -&gt; c (BooleanFormula a)
forall (t :: * -&gt; *) (c :: * -&gt; *).
Typeable t =&gt;
(forall d. Data d =&gt; c (t d)) -&gt; Maybe (c (BooleanFormula a))
forall (t :: * -&gt; * -&gt; *) (c :: * -&gt; *).
Typeable t =&gt;
(forall d e. (Data d, Data e) =&gt; c (t d e))
-&gt; Maybe (c (BooleanFormula a))
gmapMo :: forall (m :: * -&gt; *).
MonadPlus m =&gt;
(forall d. Data d =&gt; d -&gt; m d)
-&gt; BooleanFormula a -&gt; m (BooleanFormula a)
$cgmapMo :: forall a (m :: * -&gt; *).
(Data a, MonadPlus m) =&gt;
(forall d. Data d =&gt; d -&gt; m d)
-&gt; BooleanFormula a -&gt; m (BooleanFormula a)
gmapMp :: forall (m :: * -&gt; *).
MonadPlus m =&gt;
(forall d. Data d =&gt; d -&gt; m d)
-&gt; BooleanFormula a -&gt; m (BooleanFormula a)
$cgmapMp :: forall a (m :: * -&gt; *).
(Data a, MonadPlus m) =&gt;
(forall d. Data d =&gt; d -&gt; m d)
-&gt; BooleanFormula a -&gt; m (BooleanFormula a)
gmapM :: forall (m :: * -&gt; *).
Monad m =&gt;
(forall d. Data d =&gt; d -&gt; m d)
-&gt; BooleanFormula a -&gt; m (BooleanFormula a)
$cgmapM :: forall a (m :: * -&gt; *).
(Data a, Monad m) =&gt;
(forall d. Data d =&gt; d -&gt; m d)
-&gt; BooleanFormula a -&gt; m (BooleanFormula a)
gmapQi :: forall u.
Int -&gt; (forall d. Data d =&gt; d -&gt; u) -&gt; BooleanFormula a -&gt; u
$cgmapQi :: forall a u.
Data a =&gt;
Int -&gt; (forall d. Data d =&gt; d -&gt; u) -&gt; BooleanFormula a -&gt; u
gmapQ :: forall u. (forall d. Data d =&gt; d -&gt; u) -&gt; BooleanFormula a -&gt; [u]
$cgmapQ :: forall a u.
Data a =&gt;
(forall d. Data d =&gt; d -&gt; u) -&gt; BooleanFormula a -&gt; [u]
gmapQr :: forall r r'.
(r' -&gt; r -&gt; r)
-&gt; r -&gt; (forall d. Data d =&gt; d -&gt; r') -&gt; BooleanFormula a -&gt; r
$cgmapQr :: forall a r r'.
Data a =&gt;
(r' -&gt; r -&gt; r)
-&gt; r -&gt; (forall d. Data d =&gt; d -&gt; r') -&gt; BooleanFormula a -&gt; r
gmapQl :: forall r r'.
(r -&gt; r' -&gt; r)
-&gt; r -&gt; (forall d. Data d =&gt; d -&gt; r') -&gt; BooleanFormula a -&gt; r
$cgmapQl :: forall a r r'.
Data a =&gt;
(r -&gt; r' -&gt; r)
-&gt; r -&gt; (forall d. Data d =&gt; d -&gt; r') -&gt; BooleanFormula a -&gt; r
gmapT :: (forall b. Data b =&gt; b -&gt; b)
-&gt; BooleanFormula a -&gt; BooleanFormula a
$cgmapT :: forall a.
Data a =&gt;
(forall b. Data b =&gt; b -&gt; b)
-&gt; BooleanFormula a -&gt; BooleanFormula a
dataCast2 :: forall (t :: * -&gt; * -&gt; *) (c :: * -&gt; *).
Typeable t =&gt;
(forall d e. (Data d, Data e) =&gt; c (t d e))
-&gt; Maybe (c (BooleanFormula a))
$cdataCast2 :: forall a (t :: * -&gt; * -&gt; *) (c :: * -&gt; *).
(Data a, Typeable t) =&gt;
(forall d e. (Data d, Data e) =&gt; c (t d e))
-&gt; Maybe (c (BooleanFormula a))
dataCast1 :: forall (t :: * -&gt; *) (c :: * -&gt; *).
Typeable t =&gt;
(forall d. Data d =&gt; c (t d)) -&gt; Maybe (c (BooleanFormula a))
$cdataCast1 :: forall a (t :: * -&gt; *) (c :: * -&gt; *).
(Data a, Typeable t) =&gt;
(forall d. Data d =&gt; c (t d)) -&gt; Maybe (c (BooleanFormula a))
dataTypeOf :: BooleanFormula a -&gt; DataType
$cdataTypeOf :: forall a. Data a =&gt; BooleanFormula a -&gt; DataType
toConstr :: BooleanFormula a -&gt; Constr
$ctoConstr :: forall a. Data a =&gt; BooleanFormula a -&gt; Constr
gunfold :: forall (c :: * -&gt; *).
(forall b r. Data b =&gt; c (b -&gt; r) -&gt; c r)
-&gt; (forall r. r -&gt; c r) -&gt; Constr -&gt; c (BooleanFormula a)
$cgunfold :: forall a (c :: * -&gt; *).
Data a =&gt;
(forall b r. Data b =&gt; c (b -&gt; r) -&gt; c r)
-&gt; (forall r. r -&gt; c r) -&gt; Constr -&gt; c (BooleanFormula a)
gfoldl :: forall (c :: * -&gt; *).
(forall d b. Data d =&gt; c (d -&gt; b) -&gt; d -&gt; c b)
-&gt; (forall g. g -&gt; c g) -&gt; BooleanFormula a -&gt; c (BooleanFormula a)
$cgfoldl :: forall a (c :: * -&gt; *).
Data a =&gt;
(forall d b. Data d =&gt; c (d -&gt; b) -&gt; d -&gt; c b)
-&gt; (forall g. g -&gt; c g) -&gt; BooleanFormula a -&gt; c (BooleanFormula a)
</span><a href="../../base/src/Data.Data.html#Data"><span class="hs-identifier hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var">Data</span></a></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span><span class="hs-special">,</span><span> </span><span id="local-6989586621680837356"><span id="local-6989586621680837369"><span class="annot"><span class="annottext">(forall a b. (a -&gt; b) -&gt; BooleanFormula a -&gt; BooleanFormula b)
-&gt; (forall a b. a -&gt; BooleanFormula b -&gt; BooleanFormula a)
-&gt; Functor BooleanFormula
forall a b. a -&gt; BooleanFormula b -&gt; BooleanFormula a
forall a b. (a -&gt; b) -&gt; BooleanFormula a -&gt; BooleanFormula b
forall (f :: * -&gt; *).
(forall a b. (a -&gt; b) -&gt; f a -&gt; f b)
-&gt; (forall a b. a -&gt; f b -&gt; f a) -&gt; Functor f
&lt;$ :: forall a b. a -&gt; BooleanFormula b -&gt; BooleanFormula a
$c&lt;$ :: forall a b. a -&gt; BooleanFormula b -&gt; BooleanFormula a
fmap :: forall a b. (a -&gt; b) -&gt; BooleanFormula a -&gt; BooleanFormula b
$cfmap :: forall a b. (a -&gt; b) -&gt; BooleanFormula a -&gt; BooleanFormula b
</span><a href="../../base/src/GHC.Base.html#Functor"><span class="hs-identifier hs-var hs-var hs-var hs-var hs-var hs-var">Functor</span></a></span></span></span><span class="hs-special">,</span><span> </span><span id="local-6989586621680837278"><span id="local-6989586621680837280"><span id="local-6989586621680837282"><span id="local-6989586621680837284"><span id="local-6989586621680837286"><span id="local-6989586621680837288"><span id="local-6989586621680837298"><span id="local-6989586621680837300"><span id="local-6989586621680837302"><span id="local-6989586621680837304"><span id="local-6989586621680837306"><span id="local-6989586621680837308"><span id="local-6989586621680837310"><span id="local-6989586621680837320"><span id="local-6989586621680837322"><span id="local-6989586621680837343"><span id="local-6989586621680837345"><span class="annot"><span class="annottext">(forall m. Monoid m =&gt; BooleanFormula m -&gt; m)
-&gt; (forall m a. Monoid m =&gt; (a -&gt; m) -&gt; BooleanFormula a -&gt; m)
-&gt; (forall m a. Monoid m =&gt; (a -&gt; m) -&gt; BooleanFormula a -&gt; m)
-&gt; (forall a b. (a -&gt; b -&gt; b) -&gt; b -&gt; BooleanFormula a -&gt; b)
-&gt; (forall a b. (a -&gt; b -&gt; b) -&gt; b -&gt; BooleanFormula a -&gt; b)
-&gt; (forall b a. (b -&gt; a -&gt; b) -&gt; b -&gt; BooleanFormula a -&gt; b)
-&gt; (forall b a. (b -&gt; a -&gt; b) -&gt; b -&gt; BooleanFormula a -&gt; b)
-&gt; (forall a. (a -&gt; a -&gt; a) -&gt; BooleanFormula a -&gt; a)
-&gt; (forall a. (a -&gt; a -&gt; a) -&gt; BooleanFormula a -&gt; a)
-&gt; (forall a. BooleanFormula a -&gt; [a])
-&gt; (forall a. BooleanFormula a -&gt; Bool)
-&gt; (forall a. BooleanFormula a -&gt; Int)
-&gt; (forall a. Eq a =&gt; a -&gt; BooleanFormula a -&gt; Bool)
-&gt; (forall a. Ord a =&gt; BooleanFormula a -&gt; a)
-&gt; (forall a. Ord a =&gt; BooleanFormula a -&gt; a)
-&gt; (forall a. Num a =&gt; BooleanFormula a -&gt; a)
-&gt; (forall a. Num a =&gt; BooleanFormula a -&gt; a)
-&gt; Foldable BooleanFormula
forall a. Eq a =&gt; a -&gt; BooleanFormula a -&gt; Bool
forall a. Num a =&gt; BooleanFormula a -&gt; a
forall a. Ord a =&gt; BooleanFormula a -&gt; a
forall m. Monoid m =&gt; BooleanFormula m -&gt; m
forall a. BooleanFormula a -&gt; Bool
forall a. BooleanFormula a -&gt; Int
forall a. BooleanFormula a -&gt; [a]
forall a. (a -&gt; a -&gt; a) -&gt; BooleanFormula a -&gt; a
forall m a. Monoid m =&gt; (a -&gt; m) -&gt; BooleanFormula a -&gt; m
forall b a. (b -&gt; a -&gt; b) -&gt; b -&gt; BooleanFormula a -&gt; b
forall a b. (a -&gt; b -&gt; b) -&gt; b -&gt; BooleanFormula a -&gt; b
forall (t :: * -&gt; *).
(forall m. Monoid m =&gt; t m -&gt; m)
-&gt; (forall m a. Monoid m =&gt; (a -&gt; m) -&gt; t a -&gt; m)
-&gt; (forall m a. Monoid m =&gt; (a -&gt; m) -&gt; t a -&gt; m)
-&gt; (forall a b. (a -&gt; b -&gt; b) -&gt; b -&gt; t a -&gt; b)
-&gt; (forall a b. (a -&gt; b -&gt; b) -&gt; b -&gt; t a -&gt; b)
-&gt; (forall b a. (b -&gt; a -&gt; b) -&gt; b -&gt; t a -&gt; b)
-&gt; (forall b a. (b -&gt; a -&gt; b) -&gt; b -&gt; t a -&gt; b)
-&gt; (forall a. (a -&gt; a -&gt; a) -&gt; t a -&gt; a)
-&gt; (forall a. (a -&gt; a -&gt; a) -&gt; t a -&gt; a)
-&gt; (forall a. t a -&gt; [a])
-&gt; (forall a. t a -&gt; Bool)
-&gt; (forall a. t a -&gt; Int)
-&gt; (forall a. Eq a =&gt; a -&gt; t a -&gt; Bool)
-&gt; (forall a. Ord a =&gt; t a -&gt; a)
-&gt; (forall a. Ord a =&gt; t a -&gt; a)
-&gt; (forall a. Num a =&gt; t a -&gt; a)
-&gt; (forall a. Num a =&gt; t a -&gt; a)
-&gt; Foldable t
product :: forall a. Num a =&gt; BooleanFormula a -&gt; a
$cproduct :: forall a. Num a =&gt; BooleanFormula a -&gt; a
sum :: forall a. Num a =&gt; BooleanFormula a -&gt; a
$csum :: forall a. Num a =&gt; BooleanFormula a -&gt; a
minimum :: forall a. Ord a =&gt; BooleanFormula a -&gt; a
$cminimum :: forall a. Ord a =&gt; BooleanFormula a -&gt; a
maximum :: forall a. Ord a =&gt; BooleanFormula a -&gt; a
$cmaximum :: forall a. Ord a =&gt; BooleanFormula a -&gt; a
elem :: forall a. Eq a =&gt; a -&gt; BooleanFormula a -&gt; Bool
$celem :: forall a. Eq a =&gt; a -&gt; BooleanFormula a -&gt; Bool
length :: forall a. BooleanFormula a -&gt; Int
$clength :: forall a. BooleanFormula a -&gt; Int
null :: forall a. BooleanFormula a -&gt; Bool
$cnull :: forall a. BooleanFormula a -&gt; Bool
toList :: forall a. BooleanFormula a -&gt; [a]
$ctoList :: forall a. BooleanFormula a -&gt; [a]
foldl1 :: forall a. (a -&gt; a -&gt; a) -&gt; BooleanFormula a -&gt; a
$cfoldl1 :: forall a. (a -&gt; a -&gt; a) -&gt; BooleanFormula a -&gt; a
foldr1 :: forall a. (a -&gt; a -&gt; a) -&gt; BooleanFormula a -&gt; a
$cfoldr1 :: forall a. (a -&gt; a -&gt; a) -&gt; BooleanFormula a -&gt; a
foldl' :: forall b a. (b -&gt; a -&gt; b) -&gt; b -&gt; BooleanFormula a -&gt; b
$cfoldl' :: forall b a. (b -&gt; a -&gt; b) -&gt; b -&gt; BooleanFormula a -&gt; b
foldl :: forall b a. (b -&gt; a -&gt; b) -&gt; b -&gt; BooleanFormula a -&gt; b
$cfoldl :: forall b a. (b -&gt; a -&gt; b) -&gt; b -&gt; BooleanFormula a -&gt; b
foldr' :: forall a b. (a -&gt; b -&gt; b) -&gt; b -&gt; BooleanFormula a -&gt; b
$cfoldr' :: forall a b. (a -&gt; b -&gt; b) -&gt; b -&gt; BooleanFormula a -&gt; b
foldr :: forall a b. (a -&gt; b -&gt; b) -&gt; b -&gt; BooleanFormula a -&gt; b
$cfoldr :: forall a b. (a -&gt; b -&gt; b) -&gt; b -&gt; BooleanFormula a -&gt; b
foldMap' :: forall m a. Monoid m =&gt; (a -&gt; m) -&gt; BooleanFormula a -&gt; m
$cfoldMap' :: forall m a. Monoid m =&gt; (a -&gt; m) -&gt; BooleanFormula a -&gt; m
foldMap :: forall m a. Monoid m =&gt; (a -&gt; m) -&gt; BooleanFormula a -&gt; m
$cfoldMap :: forall m a. Monoid m =&gt; (a -&gt; m) -&gt; BooleanFormula a -&gt; m
fold :: forall m. Monoid m =&gt; BooleanFormula m -&gt; m
$cfold :: forall m. Monoid m =&gt; BooleanFormula m -&gt; m
</span><a href="../../base/src/Data.Foldable.html#Foldable"><span class="hs-identifier hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var">Foldable</span></a></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span></span><span class="hs-special">,</span><span> </span><span id="local-6989586621680837241"><span id="local-6989586621680837243"><span id="local-6989586621680837245"><span id="local-6989586621680837271"><span class="annot"><span class="annottext">Functor BooleanFormula
Foldable BooleanFormula
Functor BooleanFormula
-&gt; Foldable BooleanFormula
-&gt; (forall (f :: * -&gt; *) a b.
    Applicative f =&gt;
    (a -&gt; f b) -&gt; BooleanFormula a -&gt; f (BooleanFormula b))
-&gt; (forall (f :: * -&gt; *) a.
    Applicative f =&gt;
    BooleanFormula (f a) -&gt; f (BooleanFormula a))
-&gt; (forall (m :: * -&gt; *) a b.
    Monad m =&gt;
    (a -&gt; m b) -&gt; BooleanFormula a -&gt; m (BooleanFormula b))
-&gt; (forall (m :: * -&gt; *) a.
    Monad m =&gt;
    BooleanFormula (m a) -&gt; m (BooleanFormula a))
-&gt; Traversable BooleanFormula
forall (t :: * -&gt; *).
Functor t
-&gt; Foldable t
-&gt; (forall (f :: * -&gt; *) a b.
    Applicative f =&gt;
    (a -&gt; f b) -&gt; t a -&gt; f (t b))
-&gt; (forall (f :: * -&gt; *) a. Applicative f =&gt; t (f a) -&gt; f (t a))
-&gt; (forall (m :: * -&gt; *) a b.
    Monad m =&gt;
    (a -&gt; m b) -&gt; t a -&gt; m (t b))
-&gt; (forall (m :: * -&gt; *) a. Monad m =&gt; t (m a) -&gt; m (t a))
-&gt; Traversable t
forall (m :: * -&gt; *) a.
Monad m =&gt;
BooleanFormula (m a) -&gt; m (BooleanFormula a)
forall (f :: * -&gt; *) a.
Applicative f =&gt;
BooleanFormula (f a) -&gt; f (BooleanFormula a)
forall (m :: * -&gt; *) a b.
Monad m =&gt;
(a -&gt; m b) -&gt; BooleanFormula a -&gt; m (BooleanFormula b)
forall (f :: * -&gt; *) a b.
Applicative f =&gt;
(a -&gt; f b) -&gt; BooleanFormula a -&gt; f (BooleanFormula b)
sequence :: forall (m :: * -&gt; *) a.
Monad m =&gt;
BooleanFormula (m a) -&gt; m (BooleanFormula a)
$csequence :: forall (m :: * -&gt; *) a.
Monad m =&gt;
BooleanFormula (m a) -&gt; m (BooleanFormula a)
mapM :: forall (m :: * -&gt; *) a b.
Monad m =&gt;
(a -&gt; m b) -&gt; BooleanFormula a -&gt; m (BooleanFormula b)
$cmapM :: forall (m :: * -&gt; *) a b.
Monad m =&gt;
(a -&gt; m b) -&gt; BooleanFormula a -&gt; m (BooleanFormula b)
sequenceA :: forall (f :: * -&gt; *) a.
Applicative f =&gt;
BooleanFormula (f a) -&gt; f (BooleanFormula a)
$csequenceA :: forall (f :: * -&gt; *) a.
Applicative f =&gt;
BooleanFormula (f a) -&gt; f (BooleanFormula a)
traverse :: forall (f :: * -&gt; *) a b.
Applicative f =&gt;
(a -&gt; f b) -&gt; BooleanFormula a -&gt; f (BooleanFormula b)
$ctraverse :: forall (f :: * -&gt; *) a b.
Applicative f =&gt;
(a -&gt; f b) -&gt; BooleanFormula a -&gt; f (BooleanFormula b)
</span><a href="../../base/src/Data.Traversable.html#Traversable"><span class="hs-identifier hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var hs-var">Traversable</span></a></span></span></span></span></span><span class="hs-special">)</span><span>
</span><span id="line-40"></span><span>
</span><span id="line-41"></span><span id="local-6989586621680837633"><span class="annot"><a href="GHC.Data.BooleanFormula.html#mkVar"><span class="hs-identifier hs-type">mkVar</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="#local-6989586621680837633"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837633"><span class="hs-identifier hs-type">a</span></a></span></span><span>
</span><span id="line-42"></span><span id="mkVar"><span class="annot"><span class="annottext">mkVar :: forall a. a -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#mkVar"><span class="hs-identifier hs-var hs-var">mkVar</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">a -&gt; BooleanFormula a
forall a. a -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#Var"><span class="hs-identifier hs-var">Var</span></a></span><span>
</span><span id="line-43"></span><span>
</span><span id="line-44"></span><span id="local-6989586621680837631"><span class="annot"><a href="GHC.Data.BooleanFormula.html#mkFalse"><span class="hs-identifier hs-type">mkFalse</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#mkTrue"><span class="hs-identifier hs-type">mkTrue</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837631"><span class="hs-identifier hs-type">a</span></a></span></span><span>
</span><span id="line-45"></span><span id="mkFalse"><span class="annot"><span class="annottext">mkFalse :: forall a. BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#mkFalse"><span class="hs-identifier hs-var hs-var">mkFalse</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a] -&gt; BooleanFormula a
forall a. [LBooleanFormula a] -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#Or"><span class="hs-identifier hs-var">Or</span></a></span><span> </span><span class="hs-special">[</span><span class="hs-special">]</span><span>
</span><span id="line-46"></span><span id="mkTrue"><span class="annot"><span class="annottext">mkTrue :: forall a. BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#mkTrue"><span class="hs-identifier hs-var hs-var">mkTrue</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a] -&gt; BooleanFormula a
forall a. [LBooleanFormula a] -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#And"><span class="hs-identifier hs-var">And</span></a></span><span> </span><span class="hs-special">[</span><span class="hs-special">]</span><span>
</span><span id="line-47"></span><span>
</span><span id="line-48"></span><span class="hs-comment">-- Convert a Bool to a BooleanFormula</span><span>
</span><span id="line-49"></span><span id="local-6989586621680837627"><span class="annot"><a href="GHC.Data.BooleanFormula.html#mkBool"><span class="hs-identifier hs-type">mkBool</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><span class="hs-identifier hs-type">Bool</span></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837627"><span class="hs-identifier hs-type">a</span></a></span></span><span>
</span><span id="line-50"></span><span id="mkBool"><span class="annot"><span class="annottext">mkBool :: forall a. Bool -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#mkBool"><span class="hs-identifier hs-var hs-var">mkBool</span></a></span></span><span> </span><span class="annot"><span class="annottext">Bool
</span><span class="hs-identifier hs-var">False</span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">BooleanFormula a
forall a. BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#mkFalse"><span class="hs-identifier hs-var">mkFalse</span></a></span><span>
</span><span id="line-51"></span><span class="annot"><a href="GHC.Data.BooleanFormula.html#mkBool"><span class="hs-identifier hs-var">mkBool</span></a></span><span> </span><span class="annot"><span class="annottext">Bool
</span><span class="hs-identifier hs-var">True</span></span><span>  </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">BooleanFormula a
forall a. BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#mkTrue"><span class="hs-identifier hs-var">mkTrue</span></a></span><span>
</span><span id="line-52"></span><span>
</span><span id="line-53"></span><span class="hs-comment">-- Make a conjunction, and try to simplify</span><span>
</span><span id="line-54"></span><span id="local-6989586621680837625"><span class="annot"><a href="GHC.Data.BooleanFormula.html#mkAnd"><span class="hs-identifier hs-type">mkAnd</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><span class="hs-identifier hs-type">Eq</span></span><span> </span><span class="annot"><a href="#local-6989586621680837625"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="hs-special">[</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#LBooleanFormula"><span class="hs-identifier hs-type">LBooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837625"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">]</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837625"><span class="hs-identifier hs-type">a</span></a></span></span><span>
</span><span id="line-55"></span><span id="mkAnd"><span class="annot"><span class="annottext">mkAnd :: forall a. Eq a =&gt; [LBooleanFormula a] -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#mkAnd"><span class="hs-identifier hs-var hs-var">mkAnd</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">BooleanFormula a
-&gt; ([GenLocated SrcSpan (BooleanFormula a)] -&gt; BooleanFormula a)
-&gt; Maybe [GenLocated SrcSpan (BooleanFormula a)]
-&gt; BooleanFormula a
forall b a. b -&gt; (a -&gt; b) -&gt; Maybe a -&gt; b
</span><a href="../../base/src/Data.Maybe.html#maybe"><span class="hs-identifier hs-var">maybe</span></a></span><span> </span><span class="annot"><span class="annottext">BooleanFormula a
forall a. BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#mkFalse"><span class="hs-identifier hs-var">mkFalse</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)] -&gt; BooleanFormula a
forall a. [LBooleanFormula a] -&gt; BooleanFormula a
</span><a href="#local-6989586621680837230"><span class="hs-identifier hs-var">mkAnd'</span></a></span><span> </span><span class="annot"><span class="annottext">([GenLocated SrcSpan (BooleanFormula a)] -&gt; BooleanFormula a)
-&gt; ([GenLocated SrcSpan (BooleanFormula a)]
    -&gt; [GenLocated SrcSpan (BooleanFormula a)])
-&gt; [GenLocated SrcSpan (BooleanFormula a)]
-&gt; BooleanFormula a
forall b c a. (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c
</span><a href="../../base/src/GHC.Base.html#."><span class="hs-operator hs-var">.</span></a></span><span> </span><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)]
-&gt; [GenLocated SrcSpan (BooleanFormula a)]
forall a. Eq a =&gt; [a] -&gt; [a]
</span><a href="../../base/src/Data.OldList.html#nub"><span class="hs-identifier hs-var">nub</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">(Maybe [GenLocated SrcSpan (BooleanFormula a)] -&gt; BooleanFormula a)
-&gt; ([GenLocated SrcSpan (BooleanFormula a)]
    -&gt; Maybe [GenLocated SrcSpan (BooleanFormula a)])
-&gt; [GenLocated SrcSpan (BooleanFormula a)]
-&gt; BooleanFormula a
forall b c a. (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c
</span><a href="../../base/src/GHC.Base.html#."><span class="hs-operator hs-var">.</span></a></span><span> </span><span class="annot"><span class="annottext">(GenLocated SrcSpan (BooleanFormula a)
 -&gt; Maybe [GenLocated SrcSpan (BooleanFormula a)])
-&gt; [GenLocated SrcSpan (BooleanFormula a)]
-&gt; Maybe [GenLocated SrcSpan (BooleanFormula a)]
forall (m :: * -&gt; *) a b. Monad m =&gt; (a -&gt; m [b]) -&gt; [a] -&gt; m [b]
</span><a href="GHC.Utils.Monad.html#concatMapM"><span class="hs-identifier hs-var">concatMapM</span></a></span><span> </span><span class="annot"><span class="annottext">GenLocated SrcSpan (BooleanFormula a)
-&gt; Maybe [GenLocated SrcSpan (BooleanFormula a)]
forall a. LBooleanFormula a -&gt; Maybe [LBooleanFormula a]
</span><a href="#local-6989586621680837227"><span class="hs-identifier hs-var">fromAnd</span></a></span><span>
</span><span id="line-56"></span><span>  </span><span class="hs-keyword">where</span><span>
</span><span id="line-57"></span><span>  </span><span class="hs-comment">-- See Note [Simplification of BooleanFormulas]</span><span>
</span><span id="line-58"></span><span>  </span><span id="local-6989586621680837614"><span class="annot"><a href="#local-6989586621680837227"><span class="hs-identifier hs-type">fromAnd</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#LBooleanFormula"><span class="hs-identifier hs-type">LBooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837614"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="../../base/src/GHC.Maybe.html#Maybe"><span class="hs-identifier hs-type">Maybe</span></a></span><span> </span><span class="hs-special">[</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#LBooleanFormula"><span class="hs-identifier hs-type">LBooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837614"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">]</span></span><span>
</span><span id="line-59"></span><span>  </span><span id="local-6989586621680837227"><span class="annot"><span class="annottext">fromAnd :: forall a. LBooleanFormula a -&gt; Maybe [LBooleanFormula a]
</span><a href="#local-6989586621680837227"><span class="hs-identifier hs-var hs-var">fromAnd</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Types.SrcLoc.html#L"><span class="hs-identifier hs-type">L</span></a></span><span> </span><span class="annot"><span class="annottext">SrcSpan
</span><span class="hs-identifier">_</span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#And"><span class="hs-identifier hs-type">And</span></a></span><span> </span><span id="local-6989586621680837225"><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)]
</span><a href="#local-6989586621680837225"><span class="hs-identifier hs-var">xs</span></a></span></span><span class="hs-special">)</span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)]
-&gt; Maybe [GenLocated SrcSpan (BooleanFormula a)]
forall a. a -&gt; Maybe a
</span><a href="../../base/src/GHC.Maybe.html#Just"><span class="hs-identifier hs-var">Just</span></a></span><span> </span><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)]
</span><a href="#local-6989586621680837225"><span class="hs-identifier hs-var">xs</span></a></span><span>
</span><span id="line-60"></span><span>     </span><span class="hs-comment">-- assume that xs are already simplified</span><span>
</span><span id="line-61"></span><span>     </span><span class="hs-comment">-- otherwise we would need: fromAnd (And xs) = concat &lt;$&gt; traverse fromAnd xs</span><span>
</span><span id="line-62"></span><span>  </span><span class="annot"><a href="#local-6989586621680837227"><span class="hs-identifier hs-var">fromAnd</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Types.SrcLoc.html#L"><span class="hs-identifier hs-type">L</span></a></span><span> </span><span class="annot"><span class="annottext">SrcSpan
</span><span class="hs-identifier">_</span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Or"><span class="hs-identifier hs-type">Or</span></a></span><span> </span><span class="hs-special">[</span><span class="hs-special">]</span><span class="hs-special">)</span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Maybe [GenLocated SrcSpan (BooleanFormula a)]
forall a. Maybe a
</span><a href="../../base/src/GHC.Maybe.html#Nothing"><span class="hs-identifier hs-var">Nothing</span></a></span><span>
</span><span id="line-63"></span><span>     </span><span class="hs-comment">-- in case of False we bail out, And [..,mkFalse,..] == mkFalse</span><span>
</span><span id="line-64"></span><span>  </span><span class="annot"><a href="#local-6989586621680837227"><span class="hs-identifier hs-var">fromAnd</span></a></span><span> </span><span id="local-6989586621680837224"><span class="annot"><span class="annottext">GenLocated SrcSpan (BooleanFormula a)
</span><a href="#local-6989586621680837224"><span class="hs-identifier hs-var">x</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)]
-&gt; Maybe [GenLocated SrcSpan (BooleanFormula a)]
forall a. a -&gt; Maybe a
</span><a href="../../base/src/GHC.Maybe.html#Just"><span class="hs-identifier hs-var">Just</span></a></span><span> </span><span class="hs-special">[</span><span class="annot"><span class="annottext">GenLocated SrcSpan (BooleanFormula a)
</span><a href="#local-6989586621680837224"><span class="hs-identifier hs-var">x</span></a></span><span class="hs-special">]</span><span>
</span><span id="line-65"></span><span>  </span><span id="local-6989586621680837230"><span class="annot"><span class="annottext">mkAnd' :: [GenLocated SrcSpan (BooleanFormula a)] -&gt; BooleanFormula a
</span><a href="#local-6989586621680837230"><span class="hs-identifier hs-var hs-var">mkAnd'</span></a></span></span><span> </span><span class="hs-special">[</span><span id="local-6989586621680837223"><span class="annot"><span class="annottext">GenLocated SrcSpan (BooleanFormula a)
</span><a href="#local-6989586621680837223"><span class="hs-identifier hs-var">x</span></a></span></span><span class="hs-special">]</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">GenLocated SrcSpan (BooleanFormula a) -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span> </span><span class="annot"><span class="annottext">GenLocated SrcSpan (BooleanFormula a)
</span><a href="#local-6989586621680837223"><span class="hs-identifier hs-var">x</span></a></span><span>
</span><span id="line-66"></span><span>  </span><span class="annot"><a href="#local-6989586621680837230"><span class="hs-identifier hs-var">mkAnd'</span></a></span><span> </span><span id="local-6989586621680837221"><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)]
</span><a href="#local-6989586621680837221"><span class="hs-identifier hs-var">xs</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)] -&gt; BooleanFormula a
forall a. [LBooleanFormula a] -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#And"><span class="hs-identifier hs-var">And</span></a></span><span> </span><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)]
</span><a href="#local-6989586621680837221"><span class="hs-identifier hs-var">xs</span></a></span><span>
</span><span id="line-67"></span><span>
</span><span id="line-68"></span><span id="local-6989586621680837220"><span class="annot"><a href="GHC.Data.BooleanFormula.html#mkOr"><span class="hs-identifier hs-type">mkOr</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><span class="hs-identifier hs-type">Eq</span></span><span> </span><span class="annot"><a href="#local-6989586621680837220"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="hs-special">[</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#LBooleanFormula"><span class="hs-identifier hs-type">LBooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837220"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">]</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837220"><span class="hs-identifier hs-type">a</span></a></span></span><span>
</span><span id="line-69"></span><span id="mkOr"><span class="annot"><span class="annottext">mkOr :: forall a. Eq a =&gt; [LBooleanFormula a] -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#mkOr"><span class="hs-identifier hs-var hs-var">mkOr</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">BooleanFormula a
-&gt; ([GenLocated SrcSpan (BooleanFormula a)] -&gt; BooleanFormula a)
-&gt; Maybe [GenLocated SrcSpan (BooleanFormula a)]
-&gt; BooleanFormula a
forall b a. b -&gt; (a -&gt; b) -&gt; Maybe a -&gt; b
</span><a href="../../base/src/Data.Maybe.html#maybe"><span class="hs-identifier hs-var">maybe</span></a></span><span> </span><span class="annot"><span class="annottext">BooleanFormula a
forall a. BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#mkTrue"><span class="hs-identifier hs-var">mkTrue</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)] -&gt; BooleanFormula a
forall a. [LBooleanFormula a] -&gt; BooleanFormula a
</span><a href="#local-6989586621680837214"><span class="hs-identifier hs-var">mkOr'</span></a></span><span> </span><span class="annot"><span class="annottext">([GenLocated SrcSpan (BooleanFormula a)] -&gt; BooleanFormula a)
-&gt; ([GenLocated SrcSpan (BooleanFormula a)]
    -&gt; [GenLocated SrcSpan (BooleanFormula a)])
-&gt; [GenLocated SrcSpan (BooleanFormula a)]
-&gt; BooleanFormula a
forall b c a. (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c
</span><a href="../../base/src/GHC.Base.html#."><span class="hs-operator hs-var">.</span></a></span><span> </span><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)]
-&gt; [GenLocated SrcSpan (BooleanFormula a)]
forall a. Eq a =&gt; [a] -&gt; [a]
</span><a href="../../base/src/Data.OldList.html#nub"><span class="hs-identifier hs-var">nub</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">(Maybe [GenLocated SrcSpan (BooleanFormula a)] -&gt; BooleanFormula a)
-&gt; ([GenLocated SrcSpan (BooleanFormula a)]
    -&gt; Maybe [GenLocated SrcSpan (BooleanFormula a)])
-&gt; [GenLocated SrcSpan (BooleanFormula a)]
-&gt; BooleanFormula a
forall b c a. (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c
</span><a href="../../base/src/GHC.Base.html#."><span class="hs-operator hs-var">.</span></a></span><span> </span><span class="annot"><span class="annottext">(GenLocated SrcSpan (BooleanFormula a)
 -&gt; Maybe [GenLocated SrcSpan (BooleanFormula a)])
-&gt; [GenLocated SrcSpan (BooleanFormula a)]
-&gt; Maybe [GenLocated SrcSpan (BooleanFormula a)]
forall (m :: * -&gt; *) a b. Monad m =&gt; (a -&gt; m [b]) -&gt; [a] -&gt; m [b]
</span><a href="GHC.Utils.Monad.html#concatMapM"><span class="hs-identifier hs-var">concatMapM</span></a></span><span> </span><span class="annot"><span class="annottext">GenLocated SrcSpan (BooleanFormula a)
-&gt; Maybe [GenLocated SrcSpan (BooleanFormula a)]
forall a. LBooleanFormula a -&gt; Maybe [LBooleanFormula a]
</span><a href="#local-6989586621680837213"><span class="hs-identifier hs-var">fromOr</span></a></span><span>
</span><span id="line-70"></span><span>  </span><span class="hs-keyword">where</span><span>
</span><span id="line-71"></span><span>  </span><span class="hs-comment">-- See Note [Simplification of BooleanFormulas]</span><span>
</span><span id="line-72"></span><span>  </span><span id="local-6989586621680837213"><span class="annot"><span class="annottext">fromOr :: GenLocated SrcSpan (BooleanFormula a)
-&gt; Maybe [GenLocated SrcSpan (BooleanFormula a)]
</span><a href="#local-6989586621680837213"><span class="hs-identifier hs-var hs-var">fromOr</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Types.SrcLoc.html#L"><span class="hs-identifier hs-type">L</span></a></span><span> </span><span class="annot"><span class="annottext">SrcSpan
</span><span class="hs-identifier">_</span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Or"><span class="hs-identifier hs-type">Or</span></a></span><span> </span><span id="local-6989586621680837212"><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)]
</span><a href="#local-6989586621680837212"><span class="hs-identifier hs-var">xs</span></a></span></span><span class="hs-special">)</span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)]
-&gt; Maybe [GenLocated SrcSpan (BooleanFormula a)]
forall a. a -&gt; Maybe a
</span><a href="../../base/src/GHC.Maybe.html#Just"><span class="hs-identifier hs-var">Just</span></a></span><span> </span><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)]
</span><a href="#local-6989586621680837212"><span class="hs-identifier hs-var">xs</span></a></span><span>
</span><span id="line-73"></span><span>  </span><span class="annot"><a href="#local-6989586621680837213"><span class="hs-identifier hs-var">fromOr</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Types.SrcLoc.html#L"><span class="hs-identifier hs-type">L</span></a></span><span> </span><span class="annot"><span class="annottext">SrcSpan
</span><span class="hs-identifier">_</span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#And"><span class="hs-identifier hs-type">And</span></a></span><span> </span><span class="hs-special">[</span><span class="hs-special">]</span><span class="hs-special">)</span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Maybe [GenLocated SrcSpan (BooleanFormula a)]
forall a. Maybe a
</span><a href="../../base/src/GHC.Maybe.html#Nothing"><span class="hs-identifier hs-var">Nothing</span></a></span><span>
</span><span id="line-74"></span><span>  </span><span class="annot"><a href="#local-6989586621680837213"><span class="hs-identifier hs-var">fromOr</span></a></span><span> </span><span id="local-6989586621680837211"><span class="annot"><span class="annottext">GenLocated SrcSpan (BooleanFormula a)
</span><a href="#local-6989586621680837211"><span class="hs-identifier hs-var">x</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)]
-&gt; Maybe [GenLocated SrcSpan (BooleanFormula a)]
forall a. a -&gt; Maybe a
</span><a href="../../base/src/GHC.Maybe.html#Just"><span class="hs-identifier hs-var">Just</span></a></span><span> </span><span class="hs-special">[</span><span class="annot"><span class="annottext">GenLocated SrcSpan (BooleanFormula a)
</span><a href="#local-6989586621680837211"><span class="hs-identifier hs-var">x</span></a></span><span class="hs-special">]</span><span>
</span><span id="line-75"></span><span>  </span><span id="local-6989586621680837214"><span class="annot"><span class="annottext">mkOr' :: [GenLocated SrcSpan (BooleanFormula a)] -&gt; BooleanFormula a
</span><a href="#local-6989586621680837214"><span class="hs-identifier hs-var hs-var">mkOr'</span></a></span></span><span> </span><span class="hs-special">[</span><span id="local-6989586621680837210"><span class="annot"><span class="annottext">GenLocated SrcSpan (BooleanFormula a)
</span><a href="#local-6989586621680837210"><span class="hs-identifier hs-var">x</span></a></span></span><span class="hs-special">]</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">GenLocated SrcSpan (BooleanFormula a) -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span> </span><span class="annot"><span class="annottext">GenLocated SrcSpan (BooleanFormula a)
</span><a href="#local-6989586621680837210"><span class="hs-identifier hs-var">x</span></a></span><span>
</span><span id="line-76"></span><span>  </span><span class="annot"><a href="#local-6989586621680837214"><span class="hs-identifier hs-var">mkOr'</span></a></span><span> </span><span id="local-6989586621680837209"><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)]
</span><a href="#local-6989586621680837209"><span class="hs-identifier hs-var">xs</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)] -&gt; BooleanFormula a
forall a. [LBooleanFormula a] -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#Or"><span class="hs-identifier hs-var">Or</span></a></span><span> </span><span class="annot"><span class="annottext">[GenLocated SrcSpan (BooleanFormula a)]
</span><a href="#local-6989586621680837209"><span class="hs-identifier hs-var">xs</span></a></span><span>
</span><span id="line-77"></span><span>
</span><span id="line-78"></span><span>
</span><span id="line-79"></span><span class="hs-comment">{-
Note [Simplification of BooleanFormulas]
~~~~~~~~~~~~~~~~~~~~~~
The smart constructors (`mkAnd` and `mkOr`) do some attempt to simplify expressions. In particular,
 1. Collapsing nested ands and ors, so
     `(mkAnd [x, And [y,z]]`
    is represented as
     `And [x,y,z]`
    Implemented by `fromAnd`/`fromOr`
 2. Collapsing trivial ands and ors, so
     `mkAnd [x]` becomes just `x`.
    Implemented by mkAnd' / mkOr'
 3. Conjunction with false, disjunction with true is simplified, i.e.
     `mkAnd [mkFalse,x]` becomes `mkFalse`.
 4. Common subexpression elimination:
     `mkAnd [x,x,y]` is reduced to just `mkAnd [x,y]`.

This simplification is not exhaustive, in the sense that it will not produce
the smallest possible equivalent expression. For example,
`Or [And [x,y], And [x]]` could be simplified to `And [x]`, but it currently
is not. A general simplifier would need to use something like BDDs.

The reason behind the (crude) simplifier is to make for more user friendly
error messages. E.g. for the code
  &gt; class Foo a where
  &gt;     {-# MINIMAL bar, (foo, baq | foo, quux) #-}
  &gt; instance Foo Int where
  &gt;     bar = ...
  &gt;     baz = ...
  &gt;     quux = ...
We don't show a ridiculous error message like
    Implement () and (either (`foo' and ()) or (`foo' and ()))
-}</span><span>
</span><span id="line-112"></span><span>
</span><span id="line-113"></span><span class="hs-comment">----------------------------------------------------------------------</span><span>
</span><span id="line-114"></span><span class="hs-comment">-- Evaluation and simplification</span><span>
</span><span id="line-115"></span><span class="hs-comment">----------------------------------------------------------------------</span><span>
</span><span id="line-116"></span><span>
</span><span id="line-117"></span><span id="local-6989586621680837208"><span class="annot"><a href="GHC.Data.BooleanFormula.html#isFalse"><span class="hs-identifier hs-type">isFalse</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837208"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="hs-identifier hs-type">Bool</span></span></span><span>
</span><span id="line-118"></span><span id="isFalse"><span class="annot"><span class="annottext">isFalse :: forall a. BooleanFormula a -&gt; Bool
</span><a href="GHC.Data.BooleanFormula.html#isFalse"><span class="hs-identifier hs-var hs-var">isFalse</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Or"><span class="hs-identifier hs-type">Or</span></a></span><span> </span><span class="hs-special">[</span><span class="hs-special">]</span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Bool
</span><span class="hs-identifier hs-var">True</span></span><span>
</span><span id="line-119"></span><span class="annot"><a href="GHC.Data.BooleanFormula.html#isFalse"><span class="hs-identifier hs-var">isFalse</span></a></span><span> </span><span class="annot"><span class="annottext">BooleanFormula a
</span><span class="hs-identifier">_</span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Bool
</span><span class="hs-identifier hs-var">False</span></span><span>
</span><span id="line-120"></span><span>
</span><span id="line-121"></span><span id="local-6989586621680837207"><span class="annot"><a href="GHC.Data.BooleanFormula.html#isTrue"><span class="hs-identifier hs-type">isTrue</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837207"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="hs-identifier hs-type">Bool</span></span></span><span>
</span><span id="line-122"></span><span id="isTrue"><span class="annot"><span class="annottext">isTrue :: forall a. BooleanFormula a -&gt; Bool
</span><a href="GHC.Data.BooleanFormula.html#isTrue"><span class="hs-identifier hs-var hs-var">isTrue</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#And"><span class="hs-identifier hs-type">And</span></a></span><span> </span><span class="hs-special">[</span><span class="hs-special">]</span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Bool
</span><span class="hs-identifier hs-var">True</span></span><span>
</span><span id="line-123"></span><span class="annot"><a href="GHC.Data.BooleanFormula.html#isTrue"><span class="hs-identifier hs-var">isTrue</span></a></span><span> </span><span class="annot"><span class="annottext">BooleanFormula a
</span><span class="hs-identifier">_</span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Bool
</span><span class="hs-identifier hs-var">False</span></span><span>
</span><span id="line-124"></span><span>
</span><span id="line-125"></span><span id="local-6989586621680837604"><span class="annot"><a href="GHC.Data.BooleanFormula.html#eval"><span class="hs-identifier hs-type">eval</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621680837604"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="hs-identifier hs-type">Bool</span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837604"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="hs-identifier hs-type">Bool</span></span></span><span>
</span><span id="line-126"></span><span id="eval"><span class="annot"><span class="annottext">eval :: forall a. (a -&gt; Bool) -&gt; BooleanFormula a -&gt; Bool
</span><a href="GHC.Data.BooleanFormula.html#eval"><span class="hs-identifier hs-var hs-var">eval</span></a></span></span><span> </span><span id="local-6989586621680837204"><span class="annot"><span class="annottext">a -&gt; Bool
</span><a href="#local-6989586621680837204"><span class="hs-identifier hs-var">f</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Var"><span class="hs-identifier hs-type">Var</span></a></span><span> </span><span id="local-6989586621680837203"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837203"><span class="hs-identifier hs-var">x</span></a></span></span><span class="hs-special">)</span><span>  </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">a -&gt; Bool
</span><a href="#local-6989586621680837204"><span class="hs-identifier hs-var">f</span></a></span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837203"><span class="hs-identifier hs-var">x</span></a></span><span>
</span><span id="line-127"></span><span class="annot"><a href="GHC.Data.BooleanFormula.html#eval"><span class="hs-identifier hs-var">eval</span></a></span><span> </span><span id="local-6989586621680837202"><span class="annot"><span class="annottext">a -&gt; Bool
</span><a href="#local-6989586621680837202"><span class="hs-identifier hs-var">f</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#And"><span class="hs-identifier hs-type">And</span></a></span><span> </span><span id="local-6989586621680837201"><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837201"><span class="hs-identifier hs-var">xs</span></a></span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">(LBooleanFormula a -&gt; Bool) -&gt; [LBooleanFormula a] -&gt; Bool
forall (t :: * -&gt; *) a. Foldable t =&gt; (a -&gt; Bool) -&gt; t a -&gt; Bool
</span><a href="../../base/src/Data.Foldable.html#all"><span class="hs-identifier hs-var">all</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">(a -&gt; Bool) -&gt; BooleanFormula a -&gt; Bool
forall a. (a -&gt; Bool) -&gt; BooleanFormula a -&gt; Bool
</span><a href="GHC.Data.BooleanFormula.html#eval"><span class="hs-identifier hs-var">eval</span></a></span><span> </span><span class="annot"><span class="annottext">a -&gt; Bool
</span><a href="#local-6989586621680837202"><span class="hs-identifier hs-var">f</span></a></span><span> </span><span class="annot"><span class="annottext">(BooleanFormula a -&gt; Bool)
-&gt; (LBooleanFormula a -&gt; BooleanFormula a)
-&gt; LBooleanFormula a
-&gt; Bool
forall b c a. (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c
</span><a href="../../base/src/GHC.Base.html#."><span class="hs-operator hs-var">.</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837201"><span class="hs-identifier hs-var">xs</span></a></span><span>
</span><span id="line-128"></span><span class="annot"><a href="GHC.Data.BooleanFormula.html#eval"><span class="hs-identifier hs-var">eval</span></a></span><span> </span><span id="local-6989586621680837199"><span class="annot"><span class="annottext">a -&gt; Bool
</span><a href="#local-6989586621680837199"><span class="hs-identifier hs-var">f</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Or"><span class="hs-identifier hs-type">Or</span></a></span><span> </span><span id="local-6989586621680837198"><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837198"><span class="hs-identifier hs-var">xs</span></a></span></span><span class="hs-special">)</span><span>  </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">(LBooleanFormula a -&gt; Bool) -&gt; [LBooleanFormula a] -&gt; Bool
forall (t :: * -&gt; *) a. Foldable t =&gt; (a -&gt; Bool) -&gt; t a -&gt; Bool
</span><a href="../../base/src/Data.Foldable.html#any"><span class="hs-identifier hs-var">any</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">(a -&gt; Bool) -&gt; BooleanFormula a -&gt; Bool
forall a. (a -&gt; Bool) -&gt; BooleanFormula a -&gt; Bool
</span><a href="GHC.Data.BooleanFormula.html#eval"><span class="hs-identifier hs-var">eval</span></a></span><span> </span><span class="annot"><span class="annottext">a -&gt; Bool
</span><a href="#local-6989586621680837199"><span class="hs-identifier hs-var">f</span></a></span><span> </span><span class="annot"><span class="annottext">(BooleanFormula a -&gt; Bool)
-&gt; (LBooleanFormula a -&gt; BooleanFormula a)
-&gt; LBooleanFormula a
-&gt; Bool
forall b c a. (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c
</span><a href="../../base/src/GHC.Base.html#."><span class="hs-operator hs-var">.</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837198"><span class="hs-identifier hs-var">xs</span></a></span><span>
</span><span id="line-129"></span><span class="annot"><a href="GHC.Data.BooleanFormula.html#eval"><span class="hs-identifier hs-var">eval</span></a></span><span> </span><span id="local-6989586621680837196"><span class="annot"><span class="annottext">a -&gt; Bool
</span><a href="#local-6989586621680837196"><span class="hs-identifier hs-var">f</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Parens"><span class="hs-identifier hs-type">Parens</span></a></span><span> </span><span id="local-6989586621680837195"><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837195"><span class="hs-identifier hs-var">x</span></a></span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">(a -&gt; Bool) -&gt; BooleanFormula a -&gt; Bool
forall a. (a -&gt; Bool) -&gt; BooleanFormula a -&gt; Bool
</span><a href="GHC.Data.BooleanFormula.html#eval"><span class="hs-identifier hs-var">eval</span></a></span><span> </span><span class="annot"><span class="annottext">a -&gt; Bool
</span><a href="#local-6989586621680837196"><span class="hs-identifier hs-var">f</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837195"><span class="hs-identifier hs-var">x</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-130"></span><span>
</span><span id="line-131"></span><span class="hs-comment">-- Simplify a boolean formula.</span><span>
</span><span id="line-132"></span><span class="hs-comment">-- The argument function should give the truth of the atoms, or Nothing if undecided.</span><span>
</span><span id="line-133"></span><span id="local-6989586621680837600"><span class="annot"><a href="GHC.Data.BooleanFormula.html#simplify"><span class="hs-identifier hs-type">simplify</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><span class="hs-identifier hs-type">Eq</span></span><span> </span><span class="annot"><a href="#local-6989586621680837600"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621680837600"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="../../base/src/GHC.Maybe.html#Maybe"><span class="hs-identifier hs-type">Maybe</span></a></span><span> </span><span class="annot"><span class="hs-identifier hs-type">Bool</span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837600"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837600"><span class="hs-identifier hs-type">a</span></a></span></span><span>
</span><span id="line-134"></span><span id="simplify"><span class="annot"><span class="annottext">simplify :: forall a.
Eq a =&gt;
(a -&gt; Maybe Bool) -&gt; BooleanFormula a -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#simplify"><span class="hs-identifier hs-var hs-var">simplify</span></a></span></span><span> </span><span id="local-6989586621680837188"><span class="annot"><span class="annottext">a -&gt; Maybe Bool
</span><a href="#local-6989586621680837188"><span class="hs-identifier hs-var">f</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Var"><span class="hs-identifier hs-type">Var</span></a></span><span> </span><span id="local-6989586621680837187"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837187"><span class="hs-identifier hs-var">a</span></a></span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="hs-keyword">case</span><span> </span><span class="annot"><span class="annottext">a -&gt; Maybe Bool
</span><a href="#local-6989586621680837188"><span class="hs-identifier hs-var">f</span></a></span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837187"><span class="hs-identifier hs-var">a</span></a></span><span> </span><span class="hs-keyword">of</span><span>
</span><span id="line-135"></span><span>  </span><span class="annot"><span class="annottext">Maybe Bool
</span><a href="../../base/src/GHC.Maybe.html#Nothing"><span class="hs-identifier hs-var">Nothing</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">a -&gt; BooleanFormula a
forall a. a -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#Var"><span class="hs-identifier hs-var">Var</span></a></span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837187"><span class="hs-identifier hs-var">a</span></a></span><span>
</span><span id="line-136"></span><span>  </span><span class="annot"><a href="../../base/src/GHC.Maybe.html#Just"><span class="hs-identifier hs-type">Just</span></a></span><span> </span><span id="local-6989586621680837186"><span class="annot"><span class="annottext">Bool
</span><a href="#local-6989586621680837186"><span class="hs-identifier hs-var">b</span></a></span></span><span>  </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">Bool -&gt; BooleanFormula a
forall a. Bool -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#mkBool"><span class="hs-identifier hs-var">mkBool</span></a></span><span> </span><span class="annot"><span class="annottext">Bool
</span><a href="#local-6989586621680837186"><span class="hs-identifier hs-var">b</span></a></span><span>
</span><span id="line-137"></span><span class="annot"><a href="GHC.Data.BooleanFormula.html#simplify"><span class="hs-identifier hs-var">simplify</span></a></span><span> </span><span id="local-6989586621680837185"><span class="annot"><span class="annottext">a -&gt; Maybe Bool
</span><a href="#local-6989586621680837185"><span class="hs-identifier hs-var">f</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#And"><span class="hs-identifier hs-type">And</span></a></span><span> </span><span id="local-6989586621680837184"><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837184"><span class="hs-identifier hs-var">xs</span></a></span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a] -&gt; BooleanFormula a
forall a. Eq a =&gt; [LBooleanFormula a] -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#mkAnd"><span class="hs-identifier hs-var">mkAnd</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">(LBooleanFormula a -&gt; LBooleanFormula a)
-&gt; [LBooleanFormula a] -&gt; [LBooleanFormula a]
forall a b. (a -&gt; b) -&gt; [a] -&gt; [b]
</span><a href="../../base/src/GHC.Base.html#map"><span class="hs-identifier hs-var">map</span></a></span><span> </span><span class="hs-special">(</span><span class="hs-glyph">\</span><span class="hs-special">(</span><span class="annot"><a href="GHC.Types.SrcLoc.html#L"><span class="hs-identifier hs-type">L</span></a></span><span> </span><span id="local-6989586621680837183"><span class="annot"><span class="annottext">SrcSpan
</span><a href="#local-6989586621680837183"><span class="hs-identifier hs-var">l</span></a></span></span><span> </span><span id="local-6989586621680837182"><span class="annot"><span class="annottext">BooleanFormula a
</span><a href="#local-6989586621680837182"><span class="hs-identifier hs-var">x</span></a></span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">SrcSpan -&gt; BooleanFormula a -&gt; LBooleanFormula a
forall l e. l -&gt; e -&gt; GenLocated l e
</span><a href="GHC.Types.SrcLoc.html#L"><span class="hs-identifier hs-var">L</span></a></span><span> </span><span class="annot"><span class="annottext">SrcSpan
</span><a href="#local-6989586621680837183"><span class="hs-identifier hs-var">l</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">(a -&gt; Maybe Bool) -&gt; BooleanFormula a -&gt; BooleanFormula a
forall a.
Eq a =&gt;
(a -&gt; Maybe Bool) -&gt; BooleanFormula a -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#simplify"><span class="hs-identifier hs-var">simplify</span></a></span><span> </span><span class="annot"><span class="annottext">a -&gt; Maybe Bool
</span><a href="#local-6989586621680837185"><span class="hs-identifier hs-var">f</span></a></span><span> </span><span class="annot"><span class="annottext">BooleanFormula a
</span><a href="#local-6989586621680837182"><span class="hs-identifier hs-var">x</span></a></span><span class="hs-special">)</span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837184"><span class="hs-identifier hs-var">xs</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-138"></span><span class="annot"><a href="GHC.Data.BooleanFormula.html#simplify"><span class="hs-identifier hs-var">simplify</span></a></span><span> </span><span id="local-6989586621680837181"><span class="annot"><span class="annottext">a -&gt; Maybe Bool
</span><a href="#local-6989586621680837181"><span class="hs-identifier hs-var">f</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Or"><span class="hs-identifier hs-type">Or</span></a></span><span> </span><span id="local-6989586621680837180"><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837180"><span class="hs-identifier hs-var">xs</span></a></span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a] -&gt; BooleanFormula a
forall a. Eq a =&gt; [LBooleanFormula a] -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#mkOr"><span class="hs-identifier hs-var">mkOr</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">(LBooleanFormula a -&gt; LBooleanFormula a)
-&gt; [LBooleanFormula a] -&gt; [LBooleanFormula a]
forall a b. (a -&gt; b) -&gt; [a] -&gt; [b]
</span><a href="../../base/src/GHC.Base.html#map"><span class="hs-identifier hs-var">map</span></a></span><span> </span><span class="hs-special">(</span><span class="hs-glyph">\</span><span class="hs-special">(</span><span class="annot"><a href="GHC.Types.SrcLoc.html#L"><span class="hs-identifier hs-type">L</span></a></span><span> </span><span id="local-6989586621680837179"><span class="annot"><span class="annottext">SrcSpan
</span><a href="#local-6989586621680837179"><span class="hs-identifier hs-var">l</span></a></span></span><span> </span><span id="local-6989586621680837178"><span class="annot"><span class="annottext">BooleanFormula a
</span><a href="#local-6989586621680837178"><span class="hs-identifier hs-var">x</span></a></span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">SrcSpan -&gt; BooleanFormula a -&gt; LBooleanFormula a
forall l e. l -&gt; e -&gt; GenLocated l e
</span><a href="GHC.Types.SrcLoc.html#L"><span class="hs-identifier hs-var">L</span></a></span><span> </span><span class="annot"><span class="annottext">SrcSpan
</span><a href="#local-6989586621680837179"><span class="hs-identifier hs-var">l</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">(a -&gt; Maybe Bool) -&gt; BooleanFormula a -&gt; BooleanFormula a
forall a.
Eq a =&gt;
(a -&gt; Maybe Bool) -&gt; BooleanFormula a -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#simplify"><span class="hs-identifier hs-var">simplify</span></a></span><span> </span><span class="annot"><span class="annottext">a -&gt; Maybe Bool
</span><a href="#local-6989586621680837181"><span class="hs-identifier hs-var">f</span></a></span><span> </span><span class="annot"><span class="annottext">BooleanFormula a
</span><a href="#local-6989586621680837178"><span class="hs-identifier hs-var">x</span></a></span><span class="hs-special">)</span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837180"><span class="hs-identifier hs-var">xs</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-139"></span><span class="annot"><a href="GHC.Data.BooleanFormula.html#simplify"><span class="hs-identifier hs-var">simplify</span></a></span><span> </span><span id="local-6989586621680837177"><span class="annot"><span class="annottext">a -&gt; Maybe Bool
</span><a href="#local-6989586621680837177"><span class="hs-identifier hs-var">f</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Parens"><span class="hs-identifier hs-type">Parens</span></a></span><span> </span><span id="local-6989586621680837176"><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837176"><span class="hs-identifier hs-var">x</span></a></span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">(a -&gt; Maybe Bool) -&gt; BooleanFormula a -&gt; BooleanFormula a
forall a.
Eq a =&gt;
(a -&gt; Maybe Bool) -&gt; BooleanFormula a -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#simplify"><span class="hs-identifier hs-var">simplify</span></a></span><span> </span><span class="annot"><span class="annottext">a -&gt; Maybe Bool
</span><a href="#local-6989586621680837177"><span class="hs-identifier hs-var">f</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837176"><span class="hs-identifier hs-var">x</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-140"></span><span>
</span><span id="line-141"></span><span class="hs-comment">-- Test if a boolean formula is satisfied when the given values are assigned to the atoms</span><span>
</span><span id="line-142"></span><span class="hs-comment">-- if it is, returns Nothing</span><span>
</span><span id="line-143"></span><span class="hs-comment">-- if it is not, return (Just remainder)</span><span>
</span><span id="line-144"></span><span id="local-6989586621680837594"><span class="annot"><a href="GHC.Data.BooleanFormula.html#isUnsatisfied"><span class="hs-identifier hs-type">isUnsatisfied</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><span class="hs-identifier hs-type">Eq</span></span><span> </span><span class="annot"><a href="#local-6989586621680837594"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621680837594"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="hs-identifier hs-type">Bool</span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837594"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="../../base/src/GHC.Maybe.html#Maybe"><span class="hs-identifier hs-type">Maybe</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837594"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">)</span></span><span>
</span><span id="line-145"></span><span id="isUnsatisfied"><span class="annot"><span class="annottext">isUnsatisfied :: forall a.
Eq a =&gt;
(a -&gt; Bool) -&gt; BooleanFormula a -&gt; Maybe (BooleanFormula a)
</span><a href="GHC.Data.BooleanFormula.html#isUnsatisfied"><span class="hs-identifier hs-var hs-var">isUnsatisfied</span></a></span></span><span> </span><span id="local-6989586621680837174"><span class="annot"><span class="annottext">a -&gt; Bool
</span><a href="#local-6989586621680837174"><span class="hs-identifier hs-var">f</span></a></span></span><span> </span><span id="local-6989586621680837173"><span class="annot"><span class="annottext">BooleanFormula a
</span><a href="#local-6989586621680837173"><span class="hs-identifier hs-var">bf</span></a></span></span><span>
</span><span id="line-146"></span><span>    </span><span class="hs-glyph">|</span><span> </span><span class="annot"><span class="annottext">BooleanFormula a -&gt; Bool
forall a. BooleanFormula a -&gt; Bool
</span><a href="GHC.Data.BooleanFormula.html#isTrue"><span class="hs-identifier hs-var">isTrue</span></a></span><span> </span><span class="annot"><span class="annottext">BooleanFormula a
</span><a href="#local-6989586621680837172"><span class="hs-identifier hs-var">bf'</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Maybe (BooleanFormula a)
forall a. Maybe a
</span><a href="../../base/src/GHC.Maybe.html#Nothing"><span class="hs-identifier hs-var">Nothing</span></a></span><span>
</span><span id="line-147"></span><span>    </span><span class="hs-glyph">|</span><span> </span><span class="annot"><span class="annottext">Bool
</span><a href="../../base/src/GHC.Base.html#otherwise"><span class="hs-identifier hs-var">otherwise</span></a></span><span>  </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">BooleanFormula a -&gt; Maybe (BooleanFormula a)
forall a. a -&gt; Maybe a
</span><a href="../../base/src/GHC.Maybe.html#Just"><span class="hs-identifier hs-var">Just</span></a></span><span> </span><span class="annot"><span class="annottext">BooleanFormula a
</span><a href="#local-6989586621680837172"><span class="hs-identifier hs-var">bf'</span></a></span><span>
</span><span id="line-148"></span><span>  </span><span class="hs-keyword">where</span><span>
</span><span id="line-149"></span><span>  </span><span id="local-6989586621680837171"><span class="annot"><span class="annottext">f' :: a -&gt; Maybe Bool
</span><a href="#local-6989586621680837171"><span class="hs-identifier hs-var hs-var">f'</span></a></span></span><span> </span><span id="local-6989586621680837170"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837170"><span class="hs-identifier hs-var">x</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="hs-keyword">if</span><span> </span><span class="annot"><span class="annottext">a -&gt; Bool
</span><a href="#local-6989586621680837174"><span class="hs-identifier hs-var">f</span></a></span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837170"><span class="hs-identifier hs-var">x</span></a></span><span> </span><span class="hs-keyword">then</span><span> </span><span class="annot"><span class="annottext">Bool -&gt; Maybe Bool
forall a. a -&gt; Maybe a
</span><a href="../../base/src/GHC.Maybe.html#Just"><span class="hs-identifier hs-var">Just</span></a></span><span> </span><span class="annot"><span class="annottext">Bool
</span><span class="hs-identifier hs-var">True</span></span><span> </span><span class="hs-keyword">else</span><span> </span><span class="annot"><span class="annottext">Maybe Bool
forall a. Maybe a
</span><a href="../../base/src/GHC.Maybe.html#Nothing"><span class="hs-identifier hs-var">Nothing</span></a></span><span>
</span><span id="line-150"></span><span>  </span><span id="local-6989586621680837172"><span class="annot"><span class="annottext">bf' :: BooleanFormula a
</span><a href="#local-6989586621680837172"><span class="hs-identifier hs-var hs-var">bf'</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">(a -&gt; Maybe Bool) -&gt; BooleanFormula a -&gt; BooleanFormula a
forall a.
Eq a =&gt;
(a -&gt; Maybe Bool) -&gt; BooleanFormula a -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#simplify"><span class="hs-identifier hs-var">simplify</span></a></span><span> </span><span class="annot"><span class="annottext">a -&gt; Maybe Bool
</span><a href="#local-6989586621680837171"><span class="hs-identifier hs-var">f'</span></a></span><span> </span><span class="annot"><span class="annottext">BooleanFormula a
</span><a href="#local-6989586621680837173"><span class="hs-identifier hs-var">bf</span></a></span><span>
</span><span id="line-151"></span><span>
</span><span id="line-152"></span><span class="hs-comment">-- prop_simplify:</span><span>
</span><span id="line-153"></span><span class="hs-comment">--   eval f x == True   &lt;==&gt;  isTrue  (simplify (Just . f) x)</span><span>
</span><span id="line-154"></span><span class="hs-comment">--   eval f x == False  &lt;==&gt;  isFalse (simplify (Just . f) x)</span><span>
</span><span id="line-155"></span><span>
</span><span id="line-156"></span><span class="hs-comment">-- If the boolean formula holds, does that mean that the given atom is always true?</span><span>
</span><span id="line-157"></span><span id="local-6989586621680837592"><span class="annot"><a href="GHC.Data.BooleanFormula.html#impliesAtom"><span class="hs-identifier hs-type">impliesAtom</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><span class="hs-identifier hs-type">Eq</span></span><span> </span><span class="annot"><a href="#local-6989586621680837592"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837592"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="#local-6989586621680837592"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="hs-identifier hs-type">Bool</span></span></span><span>
</span><span id="line-158"></span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Var"><span class="hs-identifier hs-type">Var</span></a></span><span> </span><span id="local-6989586621680837161"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837161"><span class="hs-identifier hs-var">x</span></a></span></span><span>  </span><span id="impliesAtom"><span class="annot"><span class="annottext">impliesAtom :: forall a. Eq a =&gt; BooleanFormula a -&gt; a -&gt; Bool
</span><a href="GHC.Data.BooleanFormula.html#impliesAtom"><span class="hs-operator hs-var hs-var">`impliesAtom`</span></a></span></span><span> </span><span id="local-6989586621680837160"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837160"><span class="hs-identifier hs-var">y</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837161"><span class="hs-identifier hs-var">x</span></a></span><span> </span><span class="annot"><span class="annottext">a -&gt; a -&gt; Bool
forall a. Eq a =&gt; a -&gt; a -&gt; Bool
</span><span class="hs-operator hs-var">==</span></span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837160"><span class="hs-identifier hs-var">y</span></a></span><span>
</span><span id="line-159"></span><span class="annot"><a href="GHC.Data.BooleanFormula.html#And"><span class="hs-identifier hs-type">And</span></a></span><span> </span><span id="local-6989586621680837159"><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837159"><span class="hs-identifier hs-var">xs</span></a></span></span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#impliesAtom"><span class="hs-operator hs-var">`impliesAtom`</span></a></span><span> </span><span id="local-6989586621680837158"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837158"><span class="hs-identifier hs-var">y</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">(LBooleanFormula a -&gt; Bool) -&gt; [LBooleanFormula a] -&gt; Bool
forall (t :: * -&gt; *) a. Foldable t =&gt; (a -&gt; Bool) -&gt; t a -&gt; Bool
</span><a href="../../base/src/Data.Foldable.html#any"><span class="hs-identifier hs-var">any</span></a></span><span> </span><span class="hs-special">(</span><span class="hs-glyph">\</span><span id="local-6989586621680837157"><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837157"><span class="hs-identifier hs-var">x</span></a></span></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837157"><span class="hs-identifier hs-var">x</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">BooleanFormula a -&gt; a -&gt; Bool
forall a. Eq a =&gt; BooleanFormula a -&gt; a -&gt; Bool
</span><a href="GHC.Data.BooleanFormula.html#impliesAtom"><span class="hs-operator hs-var">`impliesAtom`</span></a></span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837158"><span class="hs-identifier hs-var">y</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837159"><span class="hs-identifier hs-var">xs</span></a></span><span>
</span><span id="line-160"></span><span>           </span><span class="hs-comment">-- we have all of xs, so one of them implying y is enough</span><span>
</span><span id="line-161"></span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Or"><span class="hs-identifier hs-type">Or</span></a></span><span>  </span><span id="local-6989586621680837156"><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837156"><span class="hs-identifier hs-var">xs</span></a></span></span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#impliesAtom"><span class="hs-operator hs-var">`impliesAtom`</span></a></span><span> </span><span id="local-6989586621680837155"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837155"><span class="hs-identifier hs-var">y</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">(LBooleanFormula a -&gt; Bool) -&gt; [LBooleanFormula a] -&gt; Bool
forall (t :: * -&gt; *) a. Foldable t =&gt; (a -&gt; Bool) -&gt; t a -&gt; Bool
</span><a href="../../base/src/Data.Foldable.html#all"><span class="hs-identifier hs-var">all</span></a></span><span> </span><span class="hs-special">(</span><span class="hs-glyph">\</span><span id="local-6989586621680837154"><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837154"><span class="hs-identifier hs-var">x</span></a></span></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837154"><span class="hs-identifier hs-var">x</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">BooleanFormula a -&gt; a -&gt; Bool
forall a. Eq a =&gt; BooleanFormula a -&gt; a -&gt; Bool
</span><a href="GHC.Data.BooleanFormula.html#impliesAtom"><span class="hs-operator hs-var">`impliesAtom`</span></a></span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837155"><span class="hs-identifier hs-var">y</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837156"><span class="hs-identifier hs-var">xs</span></a></span><span>
</span><span id="line-162"></span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Parens"><span class="hs-identifier hs-type">Parens</span></a></span><span> </span><span id="local-6989586621680837153"><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837153"><span class="hs-identifier hs-var">x</span></a></span></span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#impliesAtom"><span class="hs-operator hs-var">`impliesAtom`</span></a></span><span> </span><span id="local-6989586621680837152"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837152"><span class="hs-identifier hs-var">y</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837153"><span class="hs-identifier hs-var">x</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">BooleanFormula a -&gt; a -&gt; Bool
forall a. Eq a =&gt; BooleanFormula a -&gt; a -&gt; Bool
</span><a href="GHC.Data.BooleanFormula.html#impliesAtom"><span class="hs-operator hs-var">`impliesAtom`</span></a></span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837152"><span class="hs-identifier hs-var">y</span></a></span><span>
</span><span id="line-163"></span><span>
</span><span id="line-164"></span><span id="local-6989586621680837590"><span class="annot"><a href="GHC.Data.BooleanFormula.html#implies"><span class="hs-identifier hs-type">implies</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="GHC.Types.Unique.html#Uniquable"><span class="hs-identifier hs-type">Uniquable</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837590"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837590"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837590"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="hs-identifier hs-type">Bool</span></span></span><span>
</span><span id="line-165"></span><span id="implies"><span class="annot"><span class="annottext">implies :: forall a.
Uniquable a =&gt;
BooleanFormula a -&gt; BooleanFormula a -&gt; Bool
</span><a href="GHC.Data.BooleanFormula.html#implies"><span class="hs-identifier hs-var hs-var">implies</span></a></span></span><span> </span><span id="local-6989586621680837149"><span class="annot"><span class="annottext">BooleanFormula a
</span><a href="#local-6989586621680837149"><span class="hs-identifier hs-var">e1</span></a></span></span><span> </span><span id="local-6989586621680837148"><span class="annot"><span class="annottext">BooleanFormula a
</span><a href="#local-6989586621680837148"><span class="hs-identifier hs-var">e2</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Clause a -&gt; Clause a -&gt; Bool
forall a. Uniquable a =&gt; Clause a -&gt; Clause a -&gt; Bool
</span><a href="#local-6989586621680837147"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">UniqSet a -&gt; [BooleanFormula a] -&gt; Clause a
forall a. UniqSet a -&gt; [BooleanFormula a] -&gt; Clause a
</span><a href="GHC.Data.BooleanFormula.html#Clause"><span class="hs-identifier hs-var">Clause</span></a></span><span> </span><span class="annot"><span class="annottext">UniqSet a
forall a. UniqSet a
</span><a href="GHC.Types.Unique.Set.html#emptyUniqSet"><span class="hs-identifier hs-var">emptyUniqSet</span></a></span><span> </span><span class="hs-special">[</span><span class="annot"><span class="annottext">BooleanFormula a
</span><a href="#local-6989586621680837149"><span class="hs-identifier hs-var">e1</span></a></span><span class="hs-special">]</span><span class="hs-special">)</span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">UniqSet a -&gt; [BooleanFormula a] -&gt; Clause a
forall a. UniqSet a -&gt; [BooleanFormula a] -&gt; Clause a
</span><a href="GHC.Data.BooleanFormula.html#Clause"><span class="hs-identifier hs-var">Clause</span></a></span><span> </span><span class="annot"><span class="annottext">UniqSet a
forall a. UniqSet a
</span><a href="GHC.Types.Unique.Set.html#emptyUniqSet"><span class="hs-identifier hs-var">emptyUniqSet</span></a></span><span> </span><span class="hs-special">[</span><span class="annot"><span class="annottext">BooleanFormula a
</span><a href="#local-6989586621680837148"><span class="hs-identifier hs-var">e2</span></a></span><span class="hs-special">]</span><span class="hs-special">)</span><span>
</span><span id="line-166"></span><span>  </span><span class="hs-keyword">where</span><span>
</span><span id="line-167"></span><span>    </span><span id="local-6989586621680837586"><span class="annot"><a href="#local-6989586621680837147"><span class="hs-identifier hs-type">go</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="GHC.Types.Unique.html#Uniquable"><span class="hs-identifier hs-type">Uniquable</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837586"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Clause"><span class="hs-identifier hs-type">Clause</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837586"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Clause"><span class="hs-identifier hs-type">Clause</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837586"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="hs-identifier hs-type">Bool</span></span></span><span>
</span><span id="line-168"></span><span>    </span><span id="local-6989586621680837147"><span class="annot"><span class="annottext">go :: forall a. Uniquable a =&gt; Clause a -&gt; Clause a -&gt; Bool
</span><a href="#local-6989586621680837147"><span class="hs-identifier hs-var hs-var">go</span></a></span></span><span> </span><span id="local-6989586621680837129"><span class="annot"><span class="annottext">l :: Clause a
</span><a href="#local-6989586621680837129"><span class="hs-identifier hs-var">l</span></a></span></span><span class="hs-glyph">@</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Clause"><span class="hs-identifier hs-type">Clause</span></a></span><span class="hs-special">{</span><span> </span><span class="annot"><span class="annottext">clauseExprs :: forall a. Clause a -&gt; [BooleanFormula a]
</span><a href="GHC.Data.BooleanFormula.html#clauseExprs"><span class="hs-identifier hs-var">clauseExprs</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span id="local-6989586621680837127"><span class="annot"><span class="annottext">BooleanFormula a
</span><a href="#local-6989586621680837127"><span class="hs-identifier hs-var">hyp</span></a></span></span><span class="annot"><span class="hs-glyph hs-type">:</span></span><span id="local-6989586621680837126"><span class="annot"><span class="annottext">[BooleanFormula a]
</span><a href="#local-6989586621680837126"><span class="hs-identifier hs-var">hyps</span></a></span></span><span> </span><span class="hs-special">}</span><span> </span><span id="local-6989586621680837125"><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837125"><span class="hs-identifier hs-var">r</span></a></span></span><span> </span><span class="hs-glyph">=</span><span>
</span><span id="line-169"></span><span>        </span><span class="hs-keyword">case</span><span> </span><span class="annot"><span class="annottext">BooleanFormula a
</span><a href="#local-6989586621680837127"><span class="hs-identifier hs-var">hyp</span></a></span><span> </span><span class="hs-keyword">of</span><span>
</span><span id="line-170"></span><span>            </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Var"><span class="hs-identifier hs-type">Var</span></a></span><span> </span><span id="local-6989586621680837124"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837124"><span class="hs-identifier hs-var">x</span></a></span></span><span> </span><span class="hs-glyph">|</span><span> </span><span class="annot"><span class="annottext">a -&gt; Clause a -&gt; Bool
forall a. Uniquable a =&gt; a -&gt; Clause a -&gt; Bool
</span><a href="GHC.Data.BooleanFormula.html#memberClauseAtoms"><span class="hs-identifier hs-var">memberClauseAtoms</span></a></span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837124"><span class="hs-identifier hs-var">x</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837125"><span class="hs-identifier hs-var">r</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">Bool
</span><span class="hs-identifier hs-var">True</span></span><span>
</span><span id="line-171"></span><span>                  </span><span class="hs-glyph">|</span><span> </span><span class="annot"><span class="annottext">Bool
</span><a href="../../base/src/GHC.Base.html#otherwise"><span class="hs-identifier hs-var">otherwise</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">Clause a -&gt; Clause a -&gt; Bool
forall a. Uniquable a =&gt; Clause a -&gt; Clause a -&gt; Bool
</span><a href="#local-6989586621680837147"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">Clause a -&gt; a -&gt; Clause a
forall a. Uniquable a =&gt; Clause a -&gt; a -&gt; Clause a
</span><a href="GHC.Data.BooleanFormula.html#extendClauseAtoms"><span class="hs-identifier hs-var">extendClauseAtoms</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837129"><span class="hs-identifier hs-var">l</span></a></span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837124"><span class="hs-identifier hs-var">x</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-special">{</span><span> </span><span class="annot"><span class="annottext">clauseExprs :: [BooleanFormula a]
</span><a href="GHC.Data.BooleanFormula.html#clauseExprs"><span class="hs-identifier hs-var">clauseExprs</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">[BooleanFormula a]
</span><a href="#local-6989586621680837126"><span class="hs-identifier hs-var">hyps</span></a></span><span> </span><span class="hs-special">}</span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837125"><span class="hs-identifier hs-var">r</span></a></span><span>
</span><span id="line-172"></span><span>            </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Parens"><span class="hs-identifier hs-type">Parens</span></a></span><span> </span><span id="local-6989586621680837121"><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837121"><span class="hs-identifier hs-var">hyp'</span></a></span></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">Clause a -&gt; Clause a -&gt; Bool
forall a. Uniquable a =&gt; Clause a -&gt; Clause a -&gt; Bool
</span><a href="#local-6989586621680837147"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837129"><span class="hs-identifier hs-var">l</span></a></span><span> </span><span class="hs-special">{</span><span> </span><span class="annot"><span class="annottext">clauseExprs :: [BooleanFormula a]
</span><a href="GHC.Data.BooleanFormula.html#clauseExprs"><span class="hs-identifier hs-var">clauseExprs</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837121"><span class="hs-identifier hs-var">hyp'</span></a></span><span class="annot"><span class="annottext">BooleanFormula a -&gt; [BooleanFormula a] -&gt; [BooleanFormula a]
forall a. a -&gt; [a] -&gt; [a]
</span><span class="hs-glyph hs-var">:</span></span><span class="annot"><span class="annottext">[BooleanFormula a]
</span><a href="#local-6989586621680837126"><span class="hs-identifier hs-var">hyps</span></a></span><span> </span><span class="hs-special">}</span><span>     </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837125"><span class="hs-identifier hs-var">r</span></a></span><span>
</span><span id="line-173"></span><span>            </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#And"><span class="hs-identifier hs-type">And</span></a></span><span> </span><span id="local-6989586621680837120"><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837120"><span class="hs-identifier hs-var">hyps'</span></a></span></span><span>  </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">Clause a -&gt; Clause a -&gt; Bool
forall a. Uniquable a =&gt; Clause a -&gt; Clause a -&gt; Bool
</span><a href="#local-6989586621680837147"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837129"><span class="hs-identifier hs-var">l</span></a></span><span> </span><span class="hs-special">{</span><span> </span><span class="annot"><span class="annottext">clauseExprs :: [BooleanFormula a]
</span><a href="GHC.Data.BooleanFormula.html#clauseExprs"><span class="hs-identifier hs-var">clauseExprs</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">(LBooleanFormula a -&gt; BooleanFormula a)
-&gt; [LBooleanFormula a] -&gt; [BooleanFormula a]
forall a b. (a -&gt; b) -&gt; [a] -&gt; [b]
</span><a href="../../base/src/GHC.Base.html#map"><span class="hs-identifier hs-var">map</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837120"><span class="hs-identifier hs-var">hyps'</span></a></span><span> </span><span class="annot"><span class="annottext">[BooleanFormula a] -&gt; [BooleanFormula a] -&gt; [BooleanFormula a]
forall a. [a] -&gt; [a] -&gt; [a]
</span><a href="../../base/src/GHC.Base.html#%2B%2B"><span class="hs-operator hs-var">++</span></a></span><span> </span><span class="annot"><span class="annottext">[BooleanFormula a]
</span><a href="#local-6989586621680837126"><span class="hs-identifier hs-var">hyps</span></a></span><span> </span><span class="hs-special">}</span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837125"><span class="hs-identifier hs-var">r</span></a></span><span>
</span><span id="line-174"></span><span>            </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Or"><span class="hs-identifier hs-type">Or</span></a></span><span> </span><span id="local-6989586621680837119"><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837119"><span class="hs-identifier hs-var">hyps'</span></a></span></span><span>   </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">(LBooleanFormula a -&gt; Bool) -&gt; [LBooleanFormula a] -&gt; Bool
forall (t :: * -&gt; *) a. Foldable t =&gt; (a -&gt; Bool) -&gt; t a -&gt; Bool
</span><a href="../../base/src/Data.Foldable.html#all"><span class="hs-identifier hs-var">all</span></a></span><span> </span><span class="hs-special">(</span><span class="hs-glyph">\</span><span id="local-6989586621680837118"><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837118"><span class="hs-identifier hs-var">hyp'</span></a></span></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">Clause a -&gt; Clause a -&gt; Bool
forall a. Uniquable a =&gt; Clause a -&gt; Clause a -&gt; Bool
</span><a href="#local-6989586621680837147"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837129"><span class="hs-identifier hs-var">l</span></a></span><span> </span><span class="hs-special">{</span><span> </span><span class="annot"><span class="annottext">clauseExprs :: [BooleanFormula a]
</span><a href="GHC.Data.BooleanFormula.html#clauseExprs"><span class="hs-identifier hs-var">clauseExprs</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837118"><span class="hs-identifier hs-var">hyp'</span></a></span><span class="annot"><span class="annottext">BooleanFormula a -&gt; [BooleanFormula a] -&gt; [BooleanFormula a]
forall a. a -&gt; [a] -&gt; [a]
</span><span class="hs-glyph hs-var">:</span></span><span class="annot"><span class="annottext">[BooleanFormula a]
</span><a href="#local-6989586621680837126"><span class="hs-identifier hs-var">hyps</span></a></span><span> </span><span class="hs-special">}</span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837125"><span class="hs-identifier hs-var">r</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837119"><span class="hs-identifier hs-var">hyps'</span></a></span><span>
</span><span id="line-175"></span><span>    </span><span class="annot"><a href="#local-6989586621680837147"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span id="local-6989586621680837117"><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837117"><span class="hs-identifier hs-var">l</span></a></span></span><span> </span><span id="local-6989586621680837116"><span class="annot"><span class="annottext">r :: Clause a
</span><a href="#local-6989586621680837116"><span class="hs-identifier hs-var">r</span></a></span></span><span class="hs-glyph">@</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Clause"><span class="hs-identifier hs-type">Clause</span></a></span><span class="hs-special">{</span><span> </span><span class="annot"><span class="annottext">clauseExprs :: forall a. Clause a -&gt; [BooleanFormula a]
</span><a href="GHC.Data.BooleanFormula.html#clauseExprs"><span class="hs-identifier hs-var">clauseExprs</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span id="local-6989586621680837115"><span class="annot"><span class="annottext">BooleanFormula a
</span><a href="#local-6989586621680837115"><span class="hs-identifier hs-var">con</span></a></span></span><span class="annot"><span class="hs-glyph hs-type">:</span></span><span id="local-6989586621680837114"><span class="annot"><span class="annottext">[BooleanFormula a]
</span><a href="#local-6989586621680837114"><span class="hs-identifier hs-var">cons</span></a></span></span><span> </span><span class="hs-special">}</span><span> </span><span class="hs-glyph">=</span><span>
</span><span id="line-176"></span><span>        </span><span class="hs-keyword">case</span><span> </span><span class="annot"><span class="annottext">BooleanFormula a
</span><a href="#local-6989586621680837115"><span class="hs-identifier hs-var">con</span></a></span><span> </span><span class="hs-keyword">of</span><span>
</span><span id="line-177"></span><span>            </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Var"><span class="hs-identifier hs-type">Var</span></a></span><span> </span><span id="local-6989586621680837113"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837113"><span class="hs-identifier hs-var">x</span></a></span></span><span> </span><span class="hs-glyph">|</span><span> </span><span class="annot"><span class="annottext">a -&gt; Clause a -&gt; Bool
forall a. Uniquable a =&gt; a -&gt; Clause a -&gt; Bool
</span><a href="GHC.Data.BooleanFormula.html#memberClauseAtoms"><span class="hs-identifier hs-var">memberClauseAtoms</span></a></span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837113"><span class="hs-identifier hs-var">x</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837117"><span class="hs-identifier hs-var">l</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">Bool
</span><span class="hs-identifier hs-var">True</span></span><span>
</span><span id="line-178"></span><span>                  </span><span class="hs-glyph">|</span><span> </span><span class="annot"><span class="annottext">Bool
</span><a href="../../base/src/GHC.Base.html#otherwise"><span class="hs-identifier hs-var">otherwise</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">Clause a -&gt; Clause a -&gt; Bool
forall a. Uniquable a =&gt; Clause a -&gt; Clause a -&gt; Bool
</span><a href="#local-6989586621680837147"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837117"><span class="hs-identifier hs-var">l</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">Clause a -&gt; a -&gt; Clause a
forall a. Uniquable a =&gt; Clause a -&gt; a -&gt; Clause a
</span><a href="GHC.Data.BooleanFormula.html#extendClauseAtoms"><span class="hs-identifier hs-var">extendClauseAtoms</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837116"><span class="hs-identifier hs-var">r</span></a></span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837113"><span class="hs-identifier hs-var">x</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-special">{</span><span> </span><span class="annot"><span class="annottext">clauseExprs :: [BooleanFormula a]
</span><a href="GHC.Data.BooleanFormula.html#clauseExprs"><span class="hs-identifier hs-var">clauseExprs</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">[BooleanFormula a]
</span><a href="#local-6989586621680837114"><span class="hs-identifier hs-var">cons</span></a></span><span> </span><span class="hs-special">}</span><span>
</span><span id="line-179"></span><span>            </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Parens"><span class="hs-identifier hs-type">Parens</span></a></span><span> </span><span id="local-6989586621680837112"><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837112"><span class="hs-identifier hs-var">con'</span></a></span></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">Clause a -&gt; Clause a -&gt; Bool
forall a. Uniquable a =&gt; Clause a -&gt; Clause a -&gt; Bool
</span><a href="#local-6989586621680837147"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837117"><span class="hs-identifier hs-var">l</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837116"><span class="hs-identifier hs-var">r</span></a></span><span> </span><span class="hs-special">{</span><span> </span><span class="annot"><span class="annottext">clauseExprs :: [BooleanFormula a]
</span><a href="GHC.Data.BooleanFormula.html#clauseExprs"><span class="hs-identifier hs-var">clauseExprs</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837112"><span class="hs-identifier hs-var">con'</span></a></span><span class="annot"><span class="annottext">BooleanFormula a -&gt; [BooleanFormula a] -&gt; [BooleanFormula a]
forall a. a -&gt; [a] -&gt; [a]
</span><span class="hs-glyph hs-var">:</span></span><span class="annot"><span class="annottext">[BooleanFormula a]
</span><a href="#local-6989586621680837114"><span class="hs-identifier hs-var">cons</span></a></span><span> </span><span class="hs-special">}</span><span>
</span><span id="line-180"></span><span>            </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#And"><span class="hs-identifier hs-type">And</span></a></span><span> </span><span id="local-6989586621680837111"><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837111"><span class="hs-identifier hs-var">cons'</span></a></span></span><span>   </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">(LBooleanFormula a -&gt; Bool) -&gt; [LBooleanFormula a] -&gt; Bool
forall (t :: * -&gt; *) a. Foldable t =&gt; (a -&gt; Bool) -&gt; t a -&gt; Bool
</span><a href="../../base/src/Data.Foldable.html#all"><span class="hs-identifier hs-var">all</span></a></span><span> </span><span class="hs-special">(</span><span class="hs-glyph">\</span><span id="local-6989586621680837110"><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837110"><span class="hs-identifier hs-var">con'</span></a></span></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">Clause a -&gt; Clause a -&gt; Bool
forall a. Uniquable a =&gt; Clause a -&gt; Clause a -&gt; Bool
</span><a href="#local-6989586621680837147"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837117"><span class="hs-identifier hs-var">l</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837116"><span class="hs-identifier hs-var">r</span></a></span><span> </span><span class="hs-special">{</span><span> </span><span class="annot"><span class="annottext">clauseExprs :: [BooleanFormula a]
</span><a href="GHC.Data.BooleanFormula.html#clauseExprs"><span class="hs-identifier hs-var">clauseExprs</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837110"><span class="hs-identifier hs-var">con'</span></a></span><span class="annot"><span class="annottext">BooleanFormula a -&gt; [BooleanFormula a] -&gt; [BooleanFormula a]
forall a. a -&gt; [a] -&gt; [a]
</span><span class="hs-glyph hs-var">:</span></span><span class="annot"><span class="annottext">[BooleanFormula a]
</span><a href="#local-6989586621680837114"><span class="hs-identifier hs-var">cons</span></a></span><span> </span><span class="hs-special">}</span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837111"><span class="hs-identifier hs-var">cons'</span></a></span><span>
</span><span id="line-181"></span><span>            </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Or"><span class="hs-identifier hs-type">Or</span></a></span><span> </span><span id="local-6989586621680837109"><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837109"><span class="hs-identifier hs-var">cons'</span></a></span></span><span>    </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">Clause a -&gt; Clause a -&gt; Bool
forall a. Uniquable a =&gt; Clause a -&gt; Clause a -&gt; Bool
</span><a href="#local-6989586621680837147"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837117"><span class="hs-identifier hs-var">l</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837116"><span class="hs-identifier hs-var">r</span></a></span><span> </span><span class="hs-special">{</span><span> </span><span class="annot"><span class="annottext">clauseExprs :: [BooleanFormula a]
</span><a href="GHC.Data.BooleanFormula.html#clauseExprs"><span class="hs-identifier hs-var">clauseExprs</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">(LBooleanFormula a -&gt; BooleanFormula a)
-&gt; [LBooleanFormula a] -&gt; [BooleanFormula a]
forall a b. (a -&gt; b) -&gt; [a] -&gt; [b]
</span><a href="../../base/src/GHC.Base.html#map"><span class="hs-identifier hs-var">map</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837109"><span class="hs-identifier hs-var">cons'</span></a></span><span> </span><span class="annot"><span class="annottext">[BooleanFormula a] -&gt; [BooleanFormula a] -&gt; [BooleanFormula a]
forall a. [a] -&gt; [a] -&gt; [a]
</span><a href="../../base/src/GHC.Base.html#%2B%2B"><span class="hs-operator hs-var">++</span></a></span><span> </span><span class="annot"><span class="annottext">[BooleanFormula a]
</span><a href="#local-6989586621680837114"><span class="hs-identifier hs-var">cons</span></a></span><span> </span><span class="hs-special">}</span><span>
</span><span id="line-182"></span><span>    </span><span class="annot"><a href="#local-6989586621680837147"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><span class="hs-identifier">_</span></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><span class="hs-identifier">_</span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Bool
</span><span class="hs-identifier hs-var">False</span></span><span>
</span><span id="line-183"></span><span>
</span><span id="line-184"></span><span class="hs-comment">-- A small sequent calculus proof engine.</span><span>
</span><span id="line-185"></span><span class="hs-keyword">data</span><span> </span><span id="Clause"><span class="annot"><a href="GHC.Data.BooleanFormula.html#Clause"><span class="hs-identifier hs-var">Clause</span></a></span></span><span> </span><span id="local-6989586621680837584"><span class="annot"><a href="#local-6989586621680837584"><span class="hs-identifier hs-type">a</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span id="Clause"><span class="annot"><a href="GHC.Data.BooleanFormula.html#Clause"><span class="hs-identifier hs-var">Clause</span></a></span></span><span> </span><span class="hs-special">{</span><span>
</span><span id="line-186"></span><span>        </span><span id="clauseAtoms"><span class="annot"><span class="annottext">forall a. Clause a -&gt; UniqSet a
</span><a href="GHC.Data.BooleanFormula.html#clauseAtoms"><span class="hs-identifier hs-var hs-var">clauseAtoms</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="GHC.Types.Unique.Set.html#UniqSet"><span class="hs-identifier hs-type">UniqSet</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837584"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">,</span><span>
</span><span id="line-187"></span><span>        </span><span id="clauseExprs"><span class="annot"><span class="annottext">forall a. Clause a -&gt; [BooleanFormula a]
</span><a href="GHC.Data.BooleanFormula.html#clauseExprs"><span class="hs-identifier hs-var hs-var">clauseExprs</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="hs-special">[</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837584"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">]</span><span>
</span><span id="line-188"></span><span>    </span><span class="hs-special">}</span><span>
</span><span id="line-189"></span><span id="local-6989586621680837580"><span class="annot"><a href="GHC.Data.BooleanFormula.html#extendClauseAtoms"><span class="hs-identifier hs-type">extendClauseAtoms</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="GHC.Types.Unique.html#Uniquable"><span class="hs-identifier hs-type">Uniquable</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837580"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Clause"><span class="hs-identifier hs-type">Clause</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837580"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="#local-6989586621680837580"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Clause"><span class="hs-identifier hs-type">Clause</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837580"><span class="hs-identifier hs-type">a</span></a></span></span><span>
</span><span id="line-190"></span><span id="extendClauseAtoms"><span class="annot"><span class="annottext">extendClauseAtoms :: forall a. Uniquable a =&gt; Clause a -&gt; a -&gt; Clause a
</span><a href="GHC.Data.BooleanFormula.html#extendClauseAtoms"><span class="hs-identifier hs-var hs-var">extendClauseAtoms</span></a></span></span><span> </span><span id="local-6989586621680837105"><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837105"><span class="hs-identifier hs-var">c</span></a></span></span><span> </span><span id="local-6989586621680837104"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837104"><span class="hs-identifier hs-var">x</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837105"><span class="hs-identifier hs-var">c</span></a></span><span> </span><span class="hs-special">{</span><span> </span><span class="annot"><span class="annottext">clauseAtoms :: UniqSet a
</span><a href="GHC.Data.BooleanFormula.html#clauseAtoms"><span class="hs-identifier hs-var">clauseAtoms</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">UniqSet a -&gt; a -&gt; UniqSet a
forall a. Uniquable a =&gt; UniqSet a -&gt; a -&gt; UniqSet a
</span><a href="GHC.Types.Unique.Set.html#addOneToUniqSet"><span class="hs-identifier hs-var">addOneToUniqSet</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">Clause a -&gt; UniqSet a
forall a. Clause a -&gt; UniqSet a
</span><a href="GHC.Data.BooleanFormula.html#clauseAtoms"><span class="hs-identifier hs-var hs-var">clauseAtoms</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837105"><span class="hs-identifier hs-var">c</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837104"><span class="hs-identifier hs-var">x</span></a></span><span> </span><span class="hs-special">}</span><span>
</span><span id="line-191"></span><span>
</span><span id="line-192"></span><span id="local-6989586621680837581"><span class="annot"><a href="GHC.Data.BooleanFormula.html#memberClauseAtoms"><span class="hs-identifier hs-type">memberClauseAtoms</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="GHC.Types.Unique.html#Uniquable"><span class="hs-identifier hs-type">Uniquable</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837581"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="#local-6989586621680837581"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Clause"><span class="hs-identifier hs-type">Clause</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837581"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="hs-identifier hs-type">Bool</span></span></span><span>
</span><span id="line-193"></span><span id="memberClauseAtoms"><span class="annot"><span class="annottext">memberClauseAtoms :: forall a. Uniquable a =&gt; a -&gt; Clause a -&gt; Bool
</span><a href="GHC.Data.BooleanFormula.html#memberClauseAtoms"><span class="hs-identifier hs-var hs-var">memberClauseAtoms</span></a></span></span><span> </span><span id="local-6989586621680837100"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837100"><span class="hs-identifier hs-var">x</span></a></span></span><span> </span><span id="local-6989586621680837099"><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837099"><span class="hs-identifier hs-var">c</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837100"><span class="hs-identifier hs-var">x</span></a></span><span> </span><span class="annot"><span class="annottext">a -&gt; UniqSet a -&gt; Bool
forall a. Uniquable a =&gt; a -&gt; UniqSet a -&gt; Bool
</span><a href="GHC.Types.Unique.Set.html#elementOfUniqSet"><span class="hs-operator hs-var">`elementOfUniqSet`</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a -&gt; UniqSet a
forall a. Clause a -&gt; UniqSet a
</span><a href="GHC.Data.BooleanFormula.html#clauseAtoms"><span class="hs-identifier hs-var hs-var">clauseAtoms</span></a></span><span> </span><span class="annot"><span class="annottext">Clause a
</span><a href="#local-6989586621680837099"><span class="hs-identifier hs-var">c</span></a></span><span>
</span><span id="line-194"></span><span>
</span><span id="line-195"></span><span class="hs-comment">----------------------------------------------------------------------</span><span>
</span><span id="line-196"></span><span class="hs-comment">-- Pretty printing</span><span>
</span><span id="line-197"></span><span class="hs-comment">----------------------------------------------------------------------</span><span>
</span><span id="line-198"></span><span>
</span><span id="line-199"></span><span class="hs-comment">-- Pretty print a BooleanFormula,</span><span>
</span><span id="line-200"></span><span class="hs-comment">-- using the arguments as pretty printers for Var, And and Or respectively</span><span>
</span><span id="line-201"></span><span id="local-6989586621680837572"><span class="annot"><a href="GHC.Data.BooleanFormula.html#pprBooleanFormula%27"><span class="hs-identifier hs-type">pprBooleanFormula'</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="../../base/src/GHC.Real.html#Rational"><span class="hs-identifier hs-type">Rational</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="#local-6989586621680837572"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Utils.Outputable.html#SDoc"><span class="hs-identifier hs-type">SDoc</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-202"></span><span>                   </span><span class="hs-glyph">-&gt;</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="../../base/src/GHC.Real.html#Rational"><span class="hs-identifier hs-type">Rational</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="hs-special">[</span><span class="annot"><a href="GHC.Utils.Outputable.html#SDoc"><span class="hs-identifier hs-type">SDoc</span></a></span><span class="hs-special">]</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Utils.Outputable.html#SDoc"><span class="hs-identifier hs-type">SDoc</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-203"></span><span>                   </span><span class="hs-glyph">-&gt;</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="../../base/src/GHC.Real.html#Rational"><span class="hs-identifier hs-type">Rational</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="hs-special">[</span><span class="annot"><a href="GHC.Utils.Outputable.html#SDoc"><span class="hs-identifier hs-type">SDoc</span></a></span><span class="hs-special">]</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Utils.Outputable.html#SDoc"><span class="hs-identifier hs-type">SDoc</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-204"></span><span>                   </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="../../base/src/GHC.Real.html#Rational"><span class="hs-identifier hs-type">Rational</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837572"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Utils.Outputable.html#SDoc"><span class="hs-identifier hs-type">SDoc</span></a></span></span><span>
</span><span id="line-205"></span><span id="pprBooleanFormula%27"><span class="annot"><span class="annottext">pprBooleanFormula' :: forall a.
(Rational -&gt; a -&gt; SDoc)
-&gt; (Rational -&gt; [SDoc] -&gt; SDoc)
-&gt; (Rational -&gt; [SDoc] -&gt; SDoc)
-&gt; Rational
-&gt; BooleanFormula a
-&gt; SDoc
</span><a href="GHC.Data.BooleanFormula.html#pprBooleanFormula%27"><span class="hs-identifier hs-var hs-var">pprBooleanFormula'</span></a></span></span><span> </span><span id="local-6989586621680837096"><span class="annot"><span class="annottext">Rational -&gt; a -&gt; SDoc
</span><a href="#local-6989586621680837096"><span class="hs-identifier hs-var">pprVar</span></a></span></span><span> </span><span id="local-6989586621680837095"><span class="annot"><span class="annottext">Rational -&gt; [SDoc] -&gt; SDoc
</span><a href="#local-6989586621680837095"><span class="hs-identifier hs-var">pprAnd</span></a></span></span><span> </span><span id="local-6989586621680837094"><span class="annot"><span class="annottext">Rational -&gt; [SDoc] -&gt; SDoc
</span><a href="#local-6989586621680837094"><span class="hs-identifier hs-var">pprOr</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Rational -&gt; BooleanFormula a -&gt; SDoc
</span><a href="#local-6989586621680837093"><span class="hs-identifier hs-var">go</span></a></span><span>
</span><span id="line-206"></span><span>  </span><span class="hs-keyword">where</span><span>
</span><span id="line-207"></span><span>  </span><span id="local-6989586621680837093"><span class="annot"><span class="annottext">go :: Rational -&gt; BooleanFormula a -&gt; SDoc
</span><a href="#local-6989586621680837093"><span class="hs-identifier hs-var hs-var">go</span></a></span></span><span> </span><span id="local-6989586621680837084"><span class="annot"><span class="annottext">Rational
</span><a href="#local-6989586621680837084"><span class="hs-identifier hs-var">p</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Var"><span class="hs-identifier hs-type">Var</span></a></span><span> </span><span id="local-6989586621680837083"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837083"><span class="hs-identifier hs-var">x</span></a></span></span><span class="hs-special">)</span><span>  </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Rational -&gt; a -&gt; SDoc
</span><a href="#local-6989586621680837096"><span class="hs-identifier hs-var">pprVar</span></a></span><span> </span><span class="annot"><span class="annottext">Rational
</span><a href="#local-6989586621680837084"><span class="hs-identifier hs-var">p</span></a></span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837083"><span class="hs-identifier hs-var">x</span></a></span><span>
</span><span id="line-208"></span><span>  </span><span class="annot"><a href="#local-6989586621680837093"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span id="local-6989586621680837082"><span class="annot"><span class="annottext">Rational
</span><a href="#local-6989586621680837082"><span class="hs-identifier hs-var">p</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#And"><span class="hs-identifier hs-type">And</span></a></span><span> </span><span class="hs-special">[</span><span class="hs-special">]</span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Bool -&gt; SDoc -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#cparen"><span class="hs-identifier hs-var">cparen</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">Rational
</span><a href="#local-6989586621680837082"><span class="hs-identifier hs-var">p</span></a></span><span> </span><span class="annot"><span class="annottext">Rational -&gt; Rational -&gt; Bool
forall a. Ord a =&gt; a -&gt; a -&gt; Bool
</span><span class="hs-operator hs-var">&gt;</span></span><span> </span><span class="annot"><span class="annottext">Rational
</span><span class="hs-number">0</span></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">(SDoc -&gt; SDoc) -&gt; SDoc -&gt; SDoc
forall a b. (a -&gt; b) -&gt; a -&gt; b
</span><a href="../../base/src/GHC.Base.html#%24"><span class="hs-operator hs-var">$</span></a></span><span> </span><span class="annot"><span class="annottext">SDoc
</span><a href="GHC.Utils.Outputable.html#empty"><span class="hs-identifier hs-var">empty</span></a></span><span>
</span><span id="line-209"></span><span>  </span><span class="annot"><a href="#local-6989586621680837093"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span id="local-6989586621680837078"><span class="annot"><span class="annottext">Rational
</span><a href="#local-6989586621680837078"><span class="hs-identifier hs-var">p</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#And"><span class="hs-identifier hs-type">And</span></a></span><span> </span><span id="local-6989586621680837077"><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837077"><span class="hs-identifier hs-var">xs</span></a></span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Rational -&gt; [SDoc] -&gt; SDoc
</span><a href="#local-6989586621680837095"><span class="hs-identifier hs-var">pprAnd</span></a></span><span> </span><span class="annot"><span class="annottext">Rational
</span><a href="#local-6989586621680837078"><span class="hs-identifier hs-var">p</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">(LBooleanFormula a -&gt; SDoc) -&gt; [LBooleanFormula a] -&gt; [SDoc]
forall a b. (a -&gt; b) -&gt; [a] -&gt; [b]
</span><a href="../../base/src/GHC.Base.html#map"><span class="hs-identifier hs-var">map</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">Rational -&gt; BooleanFormula a -&gt; SDoc
</span><a href="#local-6989586621680837093"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="annot"><span class="annottext">Rational
</span><span class="hs-number">3</span></span><span> </span><span class="annot"><span class="annottext">(BooleanFormula a -&gt; SDoc)
-&gt; (LBooleanFormula a -&gt; BooleanFormula a)
-&gt; LBooleanFormula a
-&gt; SDoc
forall b c a. (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c
</span><a href="../../base/src/GHC.Base.html#."><span class="hs-operator hs-var">.</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837077"><span class="hs-identifier hs-var">xs</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-210"></span><span>  </span><span class="annot"><a href="#local-6989586621680837093"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="annot"><span class="annottext">Rational
</span><span class="hs-identifier">_</span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Or"><span class="hs-identifier hs-type">Or</span></a></span><span>  </span><span class="hs-special">[</span><span class="hs-special">]</span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">SDoc -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#keyword"><span class="hs-identifier hs-var">keyword</span></a></span><span> </span><span class="annot"><span class="annottext">(SDoc -&gt; SDoc) -&gt; SDoc -&gt; SDoc
forall a b. (a -&gt; b) -&gt; a -&gt; b
</span><a href="../../base/src/GHC.Base.html#%24"><span class="hs-operator hs-var">$</span></a></span><span> </span><span class="annot"><span class="annottext">String -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#text"><span class="hs-identifier hs-var">text</span></a></span><span> </span><span class="annot"><span class="annottext">String
</span><span class="hs-string">&quot;FALSE&quot;</span></span><span>
</span><span id="line-211"></span><span>  </span><span class="annot"><a href="#local-6989586621680837093"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span id="local-6989586621680837074"><span class="annot"><span class="annottext">Rational
</span><a href="#local-6989586621680837074"><span class="hs-identifier hs-var">p</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Or"><span class="hs-identifier hs-type">Or</span></a></span><span>  </span><span id="local-6989586621680837073"><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837073"><span class="hs-identifier hs-var">xs</span></a></span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Rational -&gt; [SDoc] -&gt; SDoc
</span><a href="#local-6989586621680837094"><span class="hs-identifier hs-var">pprOr</span></a></span><span> </span><span class="annot"><span class="annottext">Rational
</span><a href="#local-6989586621680837074"><span class="hs-identifier hs-var">p</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">(LBooleanFormula a -&gt; SDoc) -&gt; [LBooleanFormula a] -&gt; [SDoc]
forall a b. (a -&gt; b) -&gt; [a] -&gt; [b]
</span><a href="../../base/src/GHC.Base.html#map"><span class="hs-identifier hs-var">map</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">Rational -&gt; BooleanFormula a -&gt; SDoc
</span><a href="#local-6989586621680837093"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="annot"><span class="annottext">Rational
</span><span class="hs-number">2</span></span><span> </span><span class="annot"><span class="annottext">(BooleanFormula a -&gt; SDoc)
-&gt; (LBooleanFormula a -&gt; BooleanFormula a)
-&gt; LBooleanFormula a
-&gt; SDoc
forall b c a. (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c
</span><a href="../../base/src/GHC.Base.html#."><span class="hs-operator hs-var">.</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680837073"><span class="hs-identifier hs-var">xs</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-212"></span><span>  </span><span class="annot"><a href="#local-6989586621680837093"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span id="local-6989586621680837072"><span class="annot"><span class="annottext">Rational
</span><a href="#local-6989586621680837072"><span class="hs-identifier hs-var">p</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Parens"><span class="hs-identifier hs-type">Parens</span></a></span><span> </span><span id="local-6989586621680837071"><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837071"><span class="hs-identifier hs-var">x</span></a></span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Rational -&gt; BooleanFormula a -&gt; SDoc
</span><a href="#local-6989586621680837093"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="annot"><span class="annottext">Rational
</span><a href="#local-6989586621680837072"><span class="hs-identifier hs-var">p</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680837071"><span class="hs-identifier hs-var">x</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-213"></span><span>
</span><span id="line-214"></span><span class="hs-comment">-- Pretty print in source syntax, &quot;a | b | c,d,e&quot;</span><span>
</span><span id="line-215"></span><span id="local-6989586621680837563"><span class="annot"><a href="GHC.Data.BooleanFormula.html#pprBooleanFormula"><span class="hs-identifier hs-type">pprBooleanFormula</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="../../base/src/GHC.Real.html#Rational"><span class="hs-identifier hs-type">Rational</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="#local-6989586621680837563"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Utils.Outputable.html#SDoc"><span class="hs-identifier hs-type">SDoc</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="../../base/src/GHC.Real.html#Rational"><span class="hs-identifier hs-type">Rational</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837563"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Utils.Outputable.html#SDoc"><span class="hs-identifier hs-type">SDoc</span></a></span></span><span>
</span><span id="line-216"></span><span id="pprBooleanFormula"><span class="annot"><span class="annottext">pprBooleanFormula :: forall a.
(Rational -&gt; a -&gt; SDoc) -&gt; Rational -&gt; BooleanFormula a -&gt; SDoc
</span><a href="GHC.Data.BooleanFormula.html#pprBooleanFormula"><span class="hs-identifier hs-var hs-var">pprBooleanFormula</span></a></span></span><span> </span><span id="local-6989586621680837065"><span class="annot"><span class="annottext">Rational -&gt; a -&gt; SDoc
</span><a href="#local-6989586621680837065"><span class="hs-identifier hs-var">pprVar</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">(Rational -&gt; a -&gt; SDoc)
-&gt; (Rational -&gt; [SDoc] -&gt; SDoc)
-&gt; (Rational -&gt; [SDoc] -&gt; SDoc)
-&gt; Rational
-&gt; BooleanFormula a
-&gt; SDoc
forall a.
(Rational -&gt; a -&gt; SDoc)
-&gt; (Rational -&gt; [SDoc] -&gt; SDoc)
-&gt; (Rational -&gt; [SDoc] -&gt; SDoc)
-&gt; Rational
-&gt; BooleanFormula a
-&gt; SDoc
</span><a href="GHC.Data.BooleanFormula.html#pprBooleanFormula%27"><span class="hs-identifier hs-var">pprBooleanFormula'</span></a></span><span> </span><span class="annot"><span class="annottext">Rational -&gt; a -&gt; SDoc
</span><a href="#local-6989586621680837065"><span class="hs-identifier hs-var">pprVar</span></a></span><span> </span><span class="annot"><span class="annottext">Rational -&gt; [SDoc] -&gt; SDoc
forall {a}. (Ord a, Num a) =&gt; a -&gt; [SDoc] -&gt; SDoc
</span><a href="#local-6989586621680837064"><span class="hs-identifier hs-var">pprAnd</span></a></span><span> </span><span class="annot"><span class="annottext">Rational -&gt; [SDoc] -&gt; SDoc
forall {a}. (Ord a, Num a) =&gt; a -&gt; [SDoc] -&gt; SDoc
</span><a href="#local-6989586621680837063"><span class="hs-identifier hs-var">pprOr</span></a></span><span>
</span><span id="line-217"></span><span>  </span><span class="hs-keyword">where</span><span>
</span><span id="line-218"></span><span>  </span><span id="local-6989586621680837064"><span class="annot"><span class="annottext">pprAnd :: a -&gt; [SDoc] -&gt; SDoc
</span><a href="#local-6989586621680837064"><span class="hs-identifier hs-var hs-var">pprAnd</span></a></span></span><span> </span><span id="local-6989586621680837058"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837058"><span class="hs-identifier hs-var">p</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Bool -&gt; SDoc -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#cparen"><span class="hs-identifier hs-var">cparen</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837058"><span class="hs-identifier hs-var">p</span></a></span><span> </span><span class="annot"><span class="annottext">a -&gt; a -&gt; Bool
forall a. Ord a =&gt; a -&gt; a -&gt; Bool
</span><span class="hs-operator hs-var">&gt;</span></span><span> </span><span class="annot"><span class="annottext">a
</span><span class="hs-number">3</span></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">(SDoc -&gt; SDoc) -&gt; ([SDoc] -&gt; SDoc) -&gt; [SDoc] -&gt; SDoc
forall b c a. (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c
</span><a href="../../base/src/GHC.Base.html#."><span class="hs-operator hs-var">.</span></a></span><span> </span><span class="annot"><span class="annottext">[SDoc] -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#fsep"><span class="hs-identifier hs-var">fsep</span></a></span><span> </span><span class="annot"><span class="annottext">([SDoc] -&gt; SDoc) -&gt; ([SDoc] -&gt; [SDoc]) -&gt; [SDoc] -&gt; SDoc
forall b c a. (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c
</span><a href="../../base/src/GHC.Base.html#."><span class="hs-operator hs-var">.</span></a></span><span> </span><span class="annot"><span class="annottext">SDoc -&gt; [SDoc] -&gt; [SDoc]
</span><a href="GHC.Utils.Outputable.html#punctuate"><span class="hs-identifier hs-var">punctuate</span></a></span><span> </span><span class="annot"><span class="annottext">SDoc
</span><a href="GHC.Utils.Outputable.html#comma"><span class="hs-identifier hs-var">comma</span></a></span><span>
</span><span id="line-219"></span><span>  </span><span id="local-6989586621680837063"><span class="annot"><span class="annottext">pprOr :: a -&gt; [SDoc] -&gt; SDoc
</span><a href="#local-6989586621680837063"><span class="hs-identifier hs-var hs-var">pprOr</span></a></span></span><span>  </span><span id="local-6989586621680837050"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837050"><span class="hs-identifier hs-var">p</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Bool -&gt; SDoc -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#cparen"><span class="hs-identifier hs-var">cparen</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837050"><span class="hs-identifier hs-var">p</span></a></span><span> </span><span class="annot"><span class="annottext">a -&gt; a -&gt; Bool
forall a. Ord a =&gt; a -&gt; a -&gt; Bool
</span><span class="hs-operator hs-var">&gt;</span></span><span> </span><span class="annot"><span class="annottext">a
</span><span class="hs-number">2</span></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">(SDoc -&gt; SDoc) -&gt; ([SDoc] -&gt; SDoc) -&gt; [SDoc] -&gt; SDoc
forall b c a. (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c
</span><a href="../../base/src/GHC.Base.html#."><span class="hs-operator hs-var">.</span></a></span><span> </span><span class="annot"><span class="annottext">[SDoc] -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#fsep"><span class="hs-identifier hs-var">fsep</span></a></span><span> </span><span class="annot"><span class="annottext">([SDoc] -&gt; SDoc) -&gt; ([SDoc] -&gt; [SDoc]) -&gt; [SDoc] -&gt; SDoc
forall b c a. (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c
</span><a href="../../base/src/GHC.Base.html#."><span class="hs-operator hs-var">.</span></a></span><span> </span><span class="annot"><span class="annottext">SDoc -&gt; [SDoc] -&gt; [SDoc]
forall a. a -&gt; [a] -&gt; [a]
</span><a href="../../base/src/Data.OldList.html#intersperse"><span class="hs-identifier hs-var">intersperse</span></a></span><span> </span><span class="annot"><span class="annottext">SDoc
</span><a href="GHC.Utils.Outputable.html#vbar"><span class="hs-identifier hs-var">vbar</span></a></span><span>
</span><span id="line-220"></span><span>
</span><span id="line-221"></span><span class="hs-comment">-- Pretty print human in readable format, &quot;either `a' or `b' or (`c', `d' and `e')&quot;?</span><span>
</span><span id="line-222"></span><span id="local-6989586621680837559"><span class="annot"><a href="GHC.Data.BooleanFormula.html#pprBooleanFormulaNice"><span class="hs-identifier hs-type">pprBooleanFormulaNice</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="GHC.Utils.Outputable.html#Outputable"><span class="hs-identifier hs-type">Outputable</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837559"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837559"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Utils.Outputable.html#SDoc"><span class="hs-identifier hs-type">SDoc</span></a></span></span><span>
</span><span id="line-223"></span><span id="pprBooleanFormulaNice"><span class="annot"><span class="annottext">pprBooleanFormulaNice :: forall a. Outputable a =&gt; BooleanFormula a -&gt; SDoc
</span><a href="GHC.Data.BooleanFormula.html#pprBooleanFormulaNice"><span class="hs-identifier hs-var hs-var">pprBooleanFormulaNice</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">(Rational -&gt; a -&gt; SDoc)
-&gt; (Rational -&gt; [SDoc] -&gt; SDoc)
-&gt; (Rational -&gt; [SDoc] -&gt; SDoc)
-&gt; Rational
-&gt; BooleanFormula a
-&gt; SDoc
forall a.
(Rational -&gt; a -&gt; SDoc)
-&gt; (Rational -&gt; [SDoc] -&gt; SDoc)
-&gt; (Rational -&gt; [SDoc] -&gt; SDoc)
-&gt; Rational
-&gt; BooleanFormula a
-&gt; SDoc
</span><a href="GHC.Data.BooleanFormula.html#pprBooleanFormula%27"><span class="hs-identifier hs-var">pprBooleanFormula'</span></a></span><span> </span><span class="annot"><span class="annottext">Rational -&gt; a -&gt; SDoc
forall {a} {p}. Outputable a =&gt; p -&gt; a -&gt; SDoc
</span><a href="#local-6989586621680837040"><span class="hs-identifier hs-var">pprVar</span></a></span><span> </span><span class="annot"><span class="annottext">Rational -&gt; [SDoc] -&gt; SDoc
forall {a}. (Ord a, Num a) =&gt; a -&gt; [SDoc] -&gt; SDoc
</span><a href="#local-6989586621680837039"><span class="hs-identifier hs-var">pprAnd</span></a></span><span> </span><span class="annot"><span class="annottext">Rational -&gt; [SDoc] -&gt; SDoc
forall {a}. (Ord a, Num a) =&gt; a -&gt; [SDoc] -&gt; SDoc
</span><a href="#local-6989586621680837038"><span class="hs-identifier hs-var">pprOr</span></a></span><span> </span><span class="annot"><span class="annottext">Rational
</span><span class="hs-number">0</span></span><span>
</span><span id="line-224"></span><span>  </span><span class="hs-keyword">where</span><span>
</span><span id="line-225"></span><span>  </span><span id="local-6989586621680837040"><span class="annot"><span class="annottext">pprVar :: p -&gt; a -&gt; SDoc
</span><a href="#local-6989586621680837040"><span class="hs-identifier hs-var hs-var">pprVar</span></a></span></span><span> </span><span class="annot"><span class="annottext">p
</span><span class="hs-identifier">_</span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">SDoc -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#quotes"><span class="hs-identifier hs-var">quotes</span></a></span><span> </span><span class="annot"><span class="annottext">(SDoc -&gt; SDoc) -&gt; (a -&gt; SDoc) -&gt; a -&gt; SDoc
forall b c a. (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c
</span><a href="../../base/src/GHC.Base.html#."><span class="hs-operator hs-var">.</span></a></span><span> </span><span class="annot"><span class="annottext">a -&gt; SDoc
forall a. Outputable a =&gt; a -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#ppr"><span class="hs-identifier hs-var">ppr</span></a></span><span>
</span><span id="line-226"></span><span>  </span><span id="local-6989586621680837039"><span class="annot"><span class="annottext">pprAnd :: a -&gt; [SDoc] -&gt; SDoc
</span><a href="#local-6989586621680837039"><span class="hs-identifier hs-var hs-var">pprAnd</span></a></span></span><span> </span><span id="local-6989586621680837029"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837029"><span class="hs-identifier hs-var">p</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Bool -&gt; SDoc -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#cparen"><span class="hs-identifier hs-var">cparen</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837029"><span class="hs-identifier hs-var">p</span></a></span><span> </span><span class="annot"><span class="annottext">a -&gt; a -&gt; Bool
forall a. Ord a =&gt; a -&gt; a -&gt; Bool
</span><span class="hs-operator hs-var">&gt;</span></span><span> </span><span class="annot"><span class="annottext">a
</span><span class="hs-number">1</span></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">(SDoc -&gt; SDoc) -&gt; ([SDoc] -&gt; SDoc) -&gt; [SDoc] -&gt; SDoc
forall b c a. (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c
</span><a href="../../base/src/GHC.Base.html#."><span class="hs-operator hs-var">.</span></a></span><span> </span><span class="annot"><span class="annottext">[SDoc] -&gt; SDoc
</span><a href="#local-6989586621680837028"><span class="hs-identifier hs-var">pprAnd'</span></a></span><span>
</span><span id="line-227"></span><span>  </span><span id="local-6989586621680837028"><span class="annot"><span class="annottext">pprAnd' :: [SDoc] -&gt; SDoc
</span><a href="#local-6989586621680837028"><span class="hs-identifier hs-var hs-var">pprAnd'</span></a></span></span><span> </span><span class="hs-special">[</span><span class="hs-special">]</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">SDoc
</span><a href="GHC.Utils.Outputable.html#empty"><span class="hs-identifier hs-var">empty</span></a></span><span>
</span><span id="line-228"></span><span>  </span><span class="annot"><a href="#local-6989586621680837028"><span class="hs-identifier hs-var">pprAnd'</span></a></span><span> </span><span class="hs-special">[</span><span id="local-6989586621680837027"><span class="annot"><span class="annottext">SDoc
</span><a href="#local-6989586621680837027"><span class="hs-identifier hs-var">x</span></a></span></span><span class="hs-special">,</span><span id="local-6989586621680837026"><span class="annot"><span class="annottext">SDoc
</span><a href="#local-6989586621680837026"><span class="hs-identifier hs-var">y</span></a></span></span><span class="hs-special">]</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">SDoc
</span><a href="#local-6989586621680837027"><span class="hs-identifier hs-var">x</span></a></span><span> </span><span class="annot"><span class="annottext">SDoc -&gt; SDoc -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#%3C%2B%3E"><span class="hs-operator hs-var">&lt;+&gt;</span></a></span><span> </span><span class="annot"><span class="annottext">String -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#text"><span class="hs-identifier hs-var">text</span></a></span><span> </span><span class="annot"><span class="annottext">String
</span><span class="hs-string">&quot;and&quot;</span></span><span> </span><span class="annot"><span class="annottext">SDoc -&gt; SDoc -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#%3C%2B%3E"><span class="hs-operator hs-var">&lt;+&gt;</span></a></span><span> </span><span class="annot"><span class="annottext">SDoc
</span><a href="#local-6989586621680837026"><span class="hs-identifier hs-var">y</span></a></span><span>
</span><span id="line-229"></span><span>  </span><span class="annot"><a href="#local-6989586621680837028"><span class="hs-identifier hs-var">pprAnd'</span></a></span><span> </span><span id="local-6989586621680837024"><span class="annot"><span class="annottext">xs :: [SDoc]
</span><a href="#local-6989586621680837024"><span class="hs-identifier hs-var">xs</span></a></span></span><span class="hs-glyph">@</span><span class="hs-special">(</span><span class="annot"><span class="annottext">SDoc
</span><span class="hs-identifier">_</span></span><span class="annot"><span class="hs-glyph hs-type">:</span></span><span class="annot"><span class="annottext">[SDoc]
</span><span class="hs-identifier">_</span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">[SDoc] -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#fsep"><span class="hs-identifier hs-var">fsep</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">SDoc -&gt; [SDoc] -&gt; [SDoc]
</span><a href="GHC.Utils.Outputable.html#punctuate"><span class="hs-identifier hs-var">punctuate</span></a></span><span> </span><span class="annot"><span class="annottext">SDoc
</span><a href="GHC.Utils.Outputable.html#comma"><span class="hs-identifier hs-var">comma</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">[SDoc] -&gt; [SDoc]
forall a. [a] -&gt; [a]
</span><a href="../../base/src/GHC.List.html#init"><span class="hs-identifier hs-var">init</span></a></span><span> </span><span class="annot"><span class="annottext">[SDoc]
</span><a href="#local-6989586621680837024"><span class="hs-identifier hs-var">xs</span></a></span><span class="hs-special">)</span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">SDoc -&gt; SDoc -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#%3C%3E"><span class="hs-operator hs-var">&lt;&gt;</span></a></span><span> </span><span class="annot"><span class="annottext">String -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#text"><span class="hs-identifier hs-var">text</span></a></span><span> </span><span class="annot"><span class="annottext">String
</span><span class="hs-string">&quot;, and&quot;</span></span><span> </span><span class="annot"><span class="annottext">SDoc -&gt; SDoc -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#%3C%2B%3E"><span class="hs-operator hs-var">&lt;+&gt;</span></a></span><span> </span><span class="annot"><span class="annottext">[SDoc] -&gt; SDoc
forall a. [a] -&gt; a
</span><a href="../../base/src/GHC.List.html#last"><span class="hs-identifier hs-var">last</span></a></span><span> </span><span class="annot"><span class="annottext">[SDoc]
</span><a href="#local-6989586621680837024"><span class="hs-identifier hs-var">xs</span></a></span><span>
</span><span id="line-230"></span><span>  </span><span id="local-6989586621680837038"><span class="annot"><span class="annottext">pprOr :: a -&gt; [SDoc] -&gt; SDoc
</span><a href="#local-6989586621680837038"><span class="hs-identifier hs-var hs-var">pprOr</span></a></span></span><span> </span><span id="local-6989586621680837016"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837016"><span class="hs-identifier hs-var">p</span></a></span></span><span> </span><span id="local-6989586621680837015"><span class="annot"><span class="annottext">[SDoc]
</span><a href="#local-6989586621680837015"><span class="hs-identifier hs-var">xs</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Bool -&gt; SDoc -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#cparen"><span class="hs-identifier hs-var">cparen</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837016"><span class="hs-identifier hs-var">p</span></a></span><span> </span><span class="annot"><span class="annottext">a -&gt; a -&gt; Bool
forall a. Ord a =&gt; a -&gt; a -&gt; Bool
</span><span class="hs-operator hs-var">&gt;</span></span><span> </span><span class="annot"><span class="annottext">a
</span><span class="hs-number">1</span></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">(SDoc -&gt; SDoc) -&gt; SDoc -&gt; SDoc
forall a b. (a -&gt; b) -&gt; a -&gt; b
</span><a href="../../base/src/GHC.Base.html#%24"><span class="hs-operator hs-var">$</span></a></span><span> </span><span class="annot"><span class="annottext">String -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#text"><span class="hs-identifier hs-var">text</span></a></span><span> </span><span class="annot"><span class="annottext">String
</span><span class="hs-string">&quot;either&quot;</span></span><span> </span><span class="annot"><span class="annottext">SDoc -&gt; SDoc -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#%3C%2B%3E"><span class="hs-operator hs-var">&lt;+&gt;</span></a></span><span> </span><span class="annot"><span class="annottext">[SDoc] -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#sep"><span class="hs-identifier hs-var">sep</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">SDoc -&gt; [SDoc] -&gt; [SDoc]
forall a. a -&gt; [a] -&gt; [a]
</span><a href="../../base/src/Data.OldList.html#intersperse"><span class="hs-identifier hs-var">intersperse</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">String -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#text"><span class="hs-identifier hs-var">text</span></a></span><span> </span><span class="annot"><span class="annottext">String
</span><span class="hs-string">&quot;or&quot;</span></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">[SDoc]
</span><a href="#local-6989586621680837015"><span class="hs-identifier hs-var">xs</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-231"></span><span>
</span><span id="line-232"></span><span id="local-6989586621680837550"><span class="hs-keyword">instance</span><span> </span><span id="local-6989586621680837011"><span class="hs-special">(</span><span class="annot"><a href="GHC.Utils.Outputable.html#OutputableBndr"><span class="hs-identifier hs-type">OutputableBndr</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837550"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="GHC.Utils.Outputable.html#Outputable"><span class="hs-identifier hs-type">Outputable</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837550"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">)</span></span><span> </span><span class="hs-keyword">where</span><span>
</span><span id="line-233"></span><span>  </span><span id="local-6989586621680837008"><span class="annot"><span class="annottext">ppr :: BooleanFormula a -&gt; SDoc
</span><a href="#local-6989586621680837008"><span class="hs-identifier hs-var hs-var hs-var hs-var">ppr</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">BooleanFormula a -&gt; SDoc
forall a. OutputableBndr a =&gt; BooleanFormula a -&gt; SDoc
</span><a href="GHC.Data.BooleanFormula.html#pprBooleanFormulaNormal"><span class="hs-identifier hs-var">pprBooleanFormulaNormal</span></a></span></span><span>
</span><span id="line-234"></span><span>
</span><span id="line-235"></span><span id="local-6989586621680837006"><span class="annot"><a href="GHC.Data.BooleanFormula.html#pprBooleanFormulaNormal"><span class="hs-identifier hs-type">pprBooleanFormulaNormal</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Utils.Outputable.html#OutputableBndr"><span class="hs-identifier hs-type">OutputableBndr</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837006"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-236"></span><span>                        </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837006"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Utils.Outputable.html#SDoc"><span class="hs-identifier hs-type">SDoc</span></a></span></span><span>
</span><span id="line-237"></span><span id="pprBooleanFormulaNormal"><span class="annot"><span class="annottext">pprBooleanFormulaNormal :: forall a. OutputableBndr a =&gt; BooleanFormula a -&gt; SDoc
</span><a href="GHC.Data.BooleanFormula.html#pprBooleanFormulaNormal"><span class="hs-identifier hs-var hs-var">pprBooleanFormulaNormal</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">BooleanFormula a -&gt; SDoc
forall a. OutputableBndr a =&gt; BooleanFormula a -&gt; SDoc
</span><a href="#local-6989586621680837003"><span class="hs-identifier hs-var">go</span></a></span><span>
</span><span id="line-238"></span><span>  </span><span class="hs-keyword">where</span><span>
</span><span id="line-239"></span><span>    </span><span id="local-6989586621680837003"><span class="annot"><span class="annottext">go :: BooleanFormula a -&gt; SDoc
</span><a href="#local-6989586621680837003"><span class="hs-identifier hs-var hs-var">go</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Var"><span class="hs-identifier hs-type">Var</span></a></span><span> </span><span id="local-6989586621680837000"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837000"><span class="hs-identifier hs-var">x</span></a></span></span><span class="hs-special">)</span><span>    </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">a -&gt; SDoc
forall a. OutputableBndr a =&gt; a -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#pprPrefixOcc"><span class="hs-identifier hs-var">pprPrefixOcc</span></a></span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680837000"><span class="hs-identifier hs-var">x</span></a></span><span>
</span><span id="line-240"></span><span>    </span><span class="annot"><a href="#local-6989586621680837003"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#And"><span class="hs-identifier hs-type">And</span></a></span><span> </span><span id="local-6989586621680836998"><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680836998"><span class="hs-identifier hs-var">xs</span></a></span></span><span class="hs-special">)</span><span>   </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">[SDoc] -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#fsep"><span class="hs-identifier hs-var">fsep</span></a></span><span> </span><span class="annot"><span class="annottext">([SDoc] -&gt; SDoc) -&gt; [SDoc] -&gt; SDoc
forall a b. (a -&gt; b) -&gt; a -&gt; b
</span><a href="../../base/src/GHC.Base.html#%24"><span class="hs-operator hs-var">$</span></a></span><span> </span><span class="annot"><span class="annottext">SDoc -&gt; [SDoc] -&gt; [SDoc]
</span><a href="GHC.Utils.Outputable.html#punctuate"><span class="hs-identifier hs-var">punctuate</span></a></span><span> </span><span class="annot"><span class="annottext">SDoc
</span><a href="GHC.Utils.Outputable.html#comma"><span class="hs-identifier hs-var">comma</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">(LBooleanFormula a -&gt; SDoc) -&gt; [LBooleanFormula a] -&gt; [SDoc]
forall a b. (a -&gt; b) -&gt; [a] -&gt; [b]
</span><a href="../../base/src/GHC.Base.html#map"><span class="hs-identifier hs-var">map</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">BooleanFormula a -&gt; SDoc
</span><a href="#local-6989586621680837003"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="annot"><span class="annottext">(BooleanFormula a -&gt; SDoc)
-&gt; (LBooleanFormula a -&gt; BooleanFormula a)
-&gt; LBooleanFormula a
-&gt; SDoc
forall b c a. (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c
</span><a href="../../base/src/GHC.Base.html#."><span class="hs-operator hs-var">.</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680836998"><span class="hs-identifier hs-var">xs</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-241"></span><span>    </span><span class="annot"><a href="#local-6989586621680837003"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Or"><span class="hs-identifier hs-type">Or</span></a></span><span> </span><span class="hs-special">[</span><span class="hs-special">]</span><span class="hs-special">)</span><span>    </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">SDoc -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#keyword"><span class="hs-identifier hs-var">keyword</span></a></span><span> </span><span class="annot"><span class="annottext">(SDoc -&gt; SDoc) -&gt; SDoc -&gt; SDoc
forall a b. (a -&gt; b) -&gt; a -&gt; b
</span><a href="../../base/src/GHC.Base.html#%24"><span class="hs-operator hs-var">$</span></a></span><span> </span><span class="annot"><span class="annottext">String -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#text"><span class="hs-identifier hs-var">text</span></a></span><span> </span><span class="annot"><span class="annottext">String
</span><span class="hs-string">&quot;FALSE&quot;</span></span><span>
</span><span id="line-242"></span><span>    </span><span class="annot"><a href="#local-6989586621680837003"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Or"><span class="hs-identifier hs-type">Or</span></a></span><span> </span><span id="local-6989586621680836997"><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680836997"><span class="hs-identifier hs-var">xs</span></a></span></span><span class="hs-special">)</span><span>    </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">[SDoc] -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#fsep"><span class="hs-identifier hs-var">fsep</span></a></span><span> </span><span class="annot"><span class="annottext">([SDoc] -&gt; SDoc) -&gt; [SDoc] -&gt; SDoc
forall a b. (a -&gt; b) -&gt; a -&gt; b
</span><a href="../../base/src/GHC.Base.html#%24"><span class="hs-operator hs-var">$</span></a></span><span> </span><span class="annot"><span class="annottext">SDoc -&gt; [SDoc] -&gt; [SDoc]
forall a. a -&gt; [a] -&gt; [a]
</span><a href="../../base/src/Data.OldList.html#intersperse"><span class="hs-identifier hs-var">intersperse</span></a></span><span> </span><span class="annot"><span class="annottext">SDoc
</span><a href="GHC.Utils.Outputable.html#vbar"><span class="hs-identifier hs-var">vbar</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">(LBooleanFormula a -&gt; SDoc) -&gt; [LBooleanFormula a] -&gt; [SDoc]
forall a b. (a -&gt; b) -&gt; [a] -&gt; [b]
</span><a href="../../base/src/GHC.Base.html#map"><span class="hs-identifier hs-var">map</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">BooleanFormula a -&gt; SDoc
</span><a href="#local-6989586621680837003"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="annot"><span class="annottext">(BooleanFormula a -&gt; SDoc)
-&gt; (LBooleanFormula a -&gt; BooleanFormula a)
-&gt; LBooleanFormula a
-&gt; SDoc
forall b c a. (b -&gt; c) -&gt; (a -&gt; b) -&gt; a -&gt; c
</span><a href="../../base/src/GHC.Base.html#."><span class="hs-operator hs-var">.</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span class="hs-special">)</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680836997"><span class="hs-identifier hs-var">xs</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-243"></span><span>    </span><span class="annot"><a href="#local-6989586621680837003"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Parens"><span class="hs-identifier hs-type">Parens</span></a></span><span> </span><span id="local-6989586621680836996"><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680836996"><span class="hs-identifier hs-var">x</span></a></span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">SDoc -&gt; SDoc
</span><a href="GHC.Utils.Outputable.html#parens"><span class="hs-identifier hs-var">parens</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><span class="annottext">BooleanFormula a -&gt; SDoc
</span><a href="#local-6989586621680837003"><span class="hs-identifier hs-var">go</span></a></span><span> </span><span class="annot"><span class="annottext">(BooleanFormula a -&gt; SDoc) -&gt; BooleanFormula a -&gt; SDoc
forall a b. (a -&gt; b) -&gt; a -&gt; b
</span><a href="../../base/src/GHC.Base.html#%24"><span class="hs-operator hs-var">$</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall l e. GenLocated l e -&gt; e
</span><a href="GHC.Types.SrcLoc.html#unLoc"><span class="hs-identifier hs-var">unLoc</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680836996"><span class="hs-identifier hs-var">x</span></a></span><span class="hs-special">)</span><span>
</span><span id="line-244"></span><span>
</span><span id="line-245"></span><span>
</span><span id="line-246"></span><span class="hs-comment">----------------------------------------------------------------------</span><span>
</span><span id="line-247"></span><span class="hs-comment">-- Binary</span><span>
</span><span id="line-248"></span><span class="hs-comment">----------------------------------------------------------------------</span><span>
</span><span id="line-249"></span><span>
</span><span id="line-250"></span><span id="local-6989586621680837543"><span class="hs-keyword">instance</span><span> </span><span id="local-6989586621680836992"><span class="annot"><a href="GHC.Utils.Binary.html#Binary"><span class="hs-identifier hs-type">Binary</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837543"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="GHC.Utils.Binary.html#Binary"><span class="hs-identifier hs-type">Binary</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#BooleanFormula"><span class="hs-identifier hs-type">BooleanFormula</span></a></span><span> </span><span class="annot"><a href="#local-6989586621680837543"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">)</span></span><span> </span><span class="hs-keyword">where</span><span>
</span><span id="line-251"></span><span>  </span><span id="local-6989586621680836971"><span class="annot"><span class="annottext">put_ :: BinHandle -&gt; BooleanFormula a -&gt; IO ()
</span><a href="GHC.Utils.Binary.html#put_"><span class="hs-identifier hs-var hs-var hs-var hs-var">put_</span></a></span></span><span> </span><span id="local-6989586621680836969"><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836969"><span class="hs-identifier hs-var">bh</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Var"><span class="hs-identifier hs-type">Var</span></a></span><span> </span><span id="local-6989586621680836968"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680836968"><span class="hs-identifier hs-var">x</span></a></span></span><span class="hs-special">)</span><span>    </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">BinHandle -&gt; Word8 -&gt; IO ()
</span><a href="GHC.Utils.Binary.html#putByte"><span class="hs-identifier hs-var">putByte</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836969"><span class="hs-identifier hs-var">bh</span></a></span><span> </span><span class="annot"><span class="annottext">Word8
</span><span class="hs-number">0</span></span><span> </span><span class="annot"><span class="annottext">IO () -&gt; IO () -&gt; IO ()
forall (m :: * -&gt; *) a b. Monad m =&gt; m a -&gt; m b -&gt; m b
</span><a href="../../base/src/GHC.Base.html#%3E%3E"><span class="hs-operator hs-var">&gt;&gt;</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle -&gt; a -&gt; IO ()
forall a. Binary a =&gt; BinHandle -&gt; a -&gt; IO ()
</span><a href="GHC.Utils.Binary.html#put_"><span class="hs-identifier hs-var">put_</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836969"><span class="hs-identifier hs-var">bh</span></a></span><span> </span><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621680836968"><span class="hs-identifier hs-var">x</span></a></span><span>
</span><span id="line-252"></span><span>  </span><span class="annot"><a href="GHC.Utils.Binary.html#put_"><span class="hs-identifier hs-var">put_</span></a></span><span> </span><span id="local-6989586621680836966"><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836966"><span class="hs-identifier hs-var">bh</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#And"><span class="hs-identifier hs-type">And</span></a></span><span> </span><span id="local-6989586621680836965"><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680836965"><span class="hs-identifier hs-var">xs</span></a></span></span><span class="hs-special">)</span><span>   </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">BinHandle -&gt; Word8 -&gt; IO ()
</span><a href="GHC.Utils.Binary.html#putByte"><span class="hs-identifier hs-var">putByte</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836966"><span class="hs-identifier hs-var">bh</span></a></span><span> </span><span class="annot"><span class="annottext">Word8
</span><span class="hs-number">1</span></span><span> </span><span class="annot"><span class="annottext">IO () -&gt; IO () -&gt; IO ()
forall (m :: * -&gt; *) a b. Monad m =&gt; m a -&gt; m b -&gt; m b
</span><a href="../../base/src/GHC.Base.html#%3E%3E"><span class="hs-operator hs-var">&gt;&gt;</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle -&gt; [LBooleanFormula a] -&gt; IO ()
forall a. Binary a =&gt; BinHandle -&gt; a -&gt; IO ()
</span><a href="GHC.Utils.Binary.html#put_"><span class="hs-identifier hs-var">put_</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836966"><span class="hs-identifier hs-var">bh</span></a></span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680836965"><span class="hs-identifier hs-var">xs</span></a></span><span>
</span><span id="line-253"></span><span>  </span><span class="annot"><a href="GHC.Utils.Binary.html#put_"><span class="hs-identifier hs-var">put_</span></a></span><span> </span><span id="local-6989586621680836964"><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836964"><span class="hs-identifier hs-var">bh</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Or"><span class="hs-identifier hs-type">Or</span></a></span><span>  </span><span id="local-6989586621680836963"><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680836963"><span class="hs-identifier hs-var">xs</span></a></span></span><span class="hs-special">)</span><span>   </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">BinHandle -&gt; Word8 -&gt; IO ()
</span><a href="GHC.Utils.Binary.html#putByte"><span class="hs-identifier hs-var">putByte</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836964"><span class="hs-identifier hs-var">bh</span></a></span><span> </span><span class="annot"><span class="annottext">Word8
</span><span class="hs-number">2</span></span><span> </span><span class="annot"><span class="annottext">IO () -&gt; IO () -&gt; IO ()
forall (m :: * -&gt; *) a b. Monad m =&gt; m a -&gt; m b -&gt; m b
</span><a href="../../base/src/GHC.Base.html#%3E%3E"><span class="hs-operator hs-var">&gt;&gt;</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle -&gt; [LBooleanFormula a] -&gt; IO ()
forall a. Binary a =&gt; BinHandle -&gt; a -&gt; IO ()
</span><a href="GHC.Utils.Binary.html#put_"><span class="hs-identifier hs-var">put_</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836964"><span class="hs-identifier hs-var">bh</span></a></span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a]
</span><a href="#local-6989586621680836963"><span class="hs-identifier hs-var">xs</span></a></span><span>
</span><span id="line-254"></span><span>  </span><span class="annot"><a href="GHC.Utils.Binary.html#put_"><span class="hs-identifier hs-var">put_</span></a></span><span> </span><span id="local-6989586621680836962"><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836962"><span class="hs-identifier hs-var">bh</span></a></span></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="GHC.Data.BooleanFormula.html#Parens"><span class="hs-identifier hs-type">Parens</span></a></span><span> </span><span id="local-6989586621680836961"><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680836961"><span class="hs-identifier hs-var">x</span></a></span></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">BinHandle -&gt; Word8 -&gt; IO ()
</span><a href="GHC.Utils.Binary.html#putByte"><span class="hs-identifier hs-var">putByte</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836962"><span class="hs-identifier hs-var">bh</span></a></span><span> </span><span class="annot"><span class="annottext">Word8
</span><span class="hs-number">3</span></span><span> </span><span class="annot"><span class="annottext">IO () -&gt; IO () -&gt; IO ()
forall (m :: * -&gt; *) a b. Monad m =&gt; m a -&gt; m b -&gt; m b
</span><a href="../../base/src/GHC.Base.html#%3E%3E"><span class="hs-operator hs-var">&gt;&gt;</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle -&gt; LBooleanFormula a -&gt; IO ()
forall a. Binary a =&gt; BinHandle -&gt; a -&gt; IO ()
</span><a href="GHC.Utils.Binary.html#put_"><span class="hs-identifier hs-var">put_</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836962"><span class="hs-identifier hs-var">bh</span></a></span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a
</span><a href="#local-6989586621680836961"><span class="hs-identifier hs-var">x</span></a></span><span>
</span><span id="line-255"></span><span>
</span><span id="line-256"></span><span>  </span><span id="local-6989586621680836941"><span class="annot"><span class="annottext">get :: BinHandle -&gt; IO (BooleanFormula a)
</span><a href="GHC.Utils.Binary.html#get"><span class="hs-identifier hs-var hs-var hs-var hs-var">get</span></a></span></span><span> </span><span id="local-6989586621680836939"><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836939"><span class="hs-identifier hs-var">bh</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="hs-keyword">do</span><span>
</span><span id="line-257"></span><span>    </span><span id="local-6989586621680836938"><span class="annot"><span class="annottext">Word8
</span><a href="#local-6989586621680836938"><span class="hs-identifier hs-var">h</span></a></span></span><span> </span><span class="hs-glyph">&lt;-</span><span> </span><span class="annot"><span class="annottext">BinHandle -&gt; IO Word8
</span><a href="GHC.Utils.Binary.html#getByte"><span class="hs-identifier hs-var">getByte</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836939"><span class="hs-identifier hs-var">bh</span></a></span><span>
</span><span id="line-258"></span><span>    </span><span class="hs-keyword">case</span><span> </span><span class="annot"><span class="annottext">Word8
</span><a href="#local-6989586621680836938"><span class="hs-identifier hs-var">h</span></a></span><span> </span><span class="hs-keyword">of</span><span>
</span><span id="line-259"></span><span>      </span><span class="annot"><span class="annottext">Word8
</span><span class="hs-number">0</span></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">a -&gt; BooleanFormula a
forall a. a -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#Var"><span class="hs-identifier hs-var">Var</span></a></span><span>    </span><span class="annot"><span class="annottext">(a -&gt; BooleanFormula a) -&gt; IO a -&gt; IO (BooleanFormula a)
forall (f :: * -&gt; *) a b. Functor f =&gt; (a -&gt; b) -&gt; f a -&gt; f b
</span><a href="../../base/src/Data.Functor.html#%3C%24%3E"><span class="hs-operator hs-var">&lt;$&gt;</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle -&gt; IO a
forall a. Binary a =&gt; BinHandle -&gt; IO a
</span><a href="GHC.Utils.Binary.html#get"><span class="hs-identifier hs-var">get</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836939"><span class="hs-identifier hs-var">bh</span></a></span><span>
</span><span id="line-260"></span><span>      </span><span class="annot"><span class="annottext">Word8
</span><span class="hs-number">1</span></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a] -&gt; BooleanFormula a
forall a. [LBooleanFormula a] -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#And"><span class="hs-identifier hs-var">And</span></a></span><span>    </span><span class="annot"><span class="annottext">([LBooleanFormula a] -&gt; BooleanFormula a)
-&gt; IO [LBooleanFormula a] -&gt; IO (BooleanFormula a)
forall (f :: * -&gt; *) a b. Functor f =&gt; (a -&gt; b) -&gt; f a -&gt; f b
</span><a href="../../base/src/Data.Functor.html#%3C%24%3E"><span class="hs-operator hs-var">&lt;$&gt;</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle -&gt; IO [LBooleanFormula a]
forall a. Binary a =&gt; BinHandle -&gt; IO a
</span><a href="GHC.Utils.Binary.html#get"><span class="hs-identifier hs-var">get</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836939"><span class="hs-identifier hs-var">bh</span></a></span><span>
</span><span id="line-261"></span><span>      </span><span class="annot"><span class="annottext">Word8
</span><span class="hs-number">2</span></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">[LBooleanFormula a] -&gt; BooleanFormula a
forall a. [LBooleanFormula a] -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#Or"><span class="hs-identifier hs-var">Or</span></a></span><span>     </span><span class="annot"><span class="annottext">([LBooleanFormula a] -&gt; BooleanFormula a)
-&gt; IO [LBooleanFormula a] -&gt; IO (BooleanFormula a)
forall (f :: * -&gt; *) a b. Functor f =&gt; (a -&gt; b) -&gt; f a -&gt; f b
</span><a href="../../base/src/Data.Functor.html#%3C%24%3E"><span class="hs-operator hs-var">&lt;$&gt;</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle -&gt; IO [LBooleanFormula a]
forall a. Binary a =&gt; BinHandle -&gt; IO a
</span><a href="GHC.Utils.Binary.html#get"><span class="hs-identifier hs-var">get</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836939"><span class="hs-identifier hs-var">bh</span></a></span><span>
</span><span id="line-262"></span><span>      </span><span class="annot"><span class="annottext">Word8
</span><span class="hs-identifier">_</span></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><span class="annottext">LBooleanFormula a -&gt; BooleanFormula a
forall a. LBooleanFormula a -&gt; BooleanFormula a
</span><a href="GHC.Data.BooleanFormula.html#Parens"><span class="hs-identifier hs-var">Parens</span></a></span><span> </span><span class="annot"><span class="annottext">(LBooleanFormula a -&gt; BooleanFormula a)
-&gt; IO (LBooleanFormula a) -&gt; IO (BooleanFormula a)
forall (f :: * -&gt; *) a b. Functor f =&gt; (a -&gt; b) -&gt; f a -&gt; f b
</span><a href="../../base/src/Data.Functor.html#%3C%24%3E"><span class="hs-operator hs-var">&lt;$&gt;</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle -&gt; IO (LBooleanFormula a)
forall a. Binary a =&gt; BinHandle -&gt; IO a
</span><a href="GHC.Utils.Binary.html#get"><span class="hs-identifier hs-var">get</span></a></span><span> </span><span class="annot"><span class="annottext">BinHandle
</span><a href="#local-6989586621680836939"><span class="hs-identifier hs-var">bh</span></a></span></span><span>
</span><span id="line-263"></span></pre></body></html>